Skip to content
This repository has been archived by the owner on Nov 7, 2020. It is now read-only.

Home

Jump to bottom
LdBeth edited this page Oct 18, 2020 · 42 revisions

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.
  • The document generation is still working well. Still need to migrate the rest of the theories to generate full documentation.

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, it seems getting much better when safe string issue has been fixed in C files, but I'm not sure if it is relevant.
  2. improving the browser interface, need someone good at HTTP server programming, web design.
  3. Find a way to test MathBus connection.

TODO

  • consider rewrite to more idiomatic OCaml code.
  • Add fuzzy matching for cd, so one can write liFor2 for listFormation2 in the REPL.
  • continue to develop LF.
  • tear apart the repo so the theories go to a separate one.

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. Also we might use auto code generation for filter_ocaml

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.

OMake

OMake was created as the primary building system used by MetaPRL. Recent version (10.0.3) of OMake should work well. Please don't install OMake from OPAM since that one won't find out proper location of preset files, so just build and install from source.

Clone this wiki locally