Home

Welcome to the metaprl wiki!

Progress on porting

with OCaml 4.11 and CamlP5 8.00-alpha 7.12 7.13 for 7.12 lacks cmx version of some files.

DONE

• figure out how to use omake.
• start work on github source instead of old svn version
• fix macro preprocessor on CamlP5
• custom ocamldep already works
• generate macro preprocessor executable now works without patching CamlP5
• libmojave shall no more be problematic
• The shell interface is working now, browsing theory itt/core shall not be a problem
• fixed parsing negative number, temporarily by handler a special case of - application
• fixed Ploc filename causes `check' not working
• refiner shows no problem
• solved exported theory file checksum overflow.

WIP

HIGH PIRO

1. Disable saving if theorems are just checked?
2. Get to understand new CamlP5 8.00 API, finish migration.
   • Completely rewrite filter_ocaml, consider using some code generation techniques.
   • Workout the term grammar, figuring out the lexing issue.
3. Working with CamlP5 developers for filter module porting.

LOW PIOR

1. http server sometimes SIGSEGV
2. improving the browser interface, need someone good a HTTP server, web design.

TODO

• test document tool set. latex stuff, etc.
• consider rewrite to more idiomatic OCaml code.

flambda

Please don't use flambda, it is currently incompatible due to cross module optimization not work well with make style building systems. See https://github.com/ocaml/ocaml/issues/7645

CamlP5 7.13

• main/pcaml.cmx and main/reloc.cmx needs to be copied to camlp5 install dir

CamlP5 8.00 API

The 8.00-alpha API is undocumented, however syntax changes can be referred in https://github.com/camlp5/camlp5/blob/master/test/quot_r.ml

Ensemble

The Ensemble based distributed refiner haven't been used in MetaPRL for a long period. Ensemble has been revived in https://github.com/chetmurthy/ensemble and the latest version works on 4.10.0.