Home

Welcome to the metaprl wiki!

Progress on porting

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

Please consider leave a message here if you're interested in contributing/using MetaPRL.

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.
• Good news is document generation is still working well. Still need to figure out how to use OMake to generate documents though.

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. Consider remove some never used features, such as OOP.
   • Workout the term grammar, implement a replacement to pa_o with minimal supports to OCaml grammar. First test this grammar on 7.13 branch.
   • 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

• 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

PPX

Consider add "hashconsing" to term data structures.

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.