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 Nov 7, 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 working well. Although some styling issue should be fixed.
  • fix Lm_num hashing issue by replace the bigint implementation by Zarith.
  • revive ITT tests.
  • fixed looping bug in libmojave’s MakePrintf
  • use functions from Zarith in tactics.

WIP

  • figuring out the Omega tests, JProver etc.
    • arithT cannot find contradiction in <Γ>; (3 * a)≥1; (2 * a)≤1 ⊢ False

HIGH PIRO

  1. 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.
  4. Improve mprun, the OCaml repl, figuring out how Shell_p4 work with the toplevel.
  5. Libmojave's MakePrintf haven't been used much in MetaPRL, maybe should just consider remove it.

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 theory.
  • tear apart the repo so the theories go to a separate one.
  • use ocamlfind for dependency management.
  • move from pa_macro to cppo for preprocessor.
  • currently, theories cannot be displayed if they are not sub theories of Shell. Try improve this mechanism.
  • the result program is about 40MB if whole itt theory is linked, which slows down the startup time, consider load theory modules after toplevel gets started.
  • develop computational theories, corecursion, etc from NuPRL.

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.

Zarith

MetaPRL now depends on Zarith, which requires either GMP or MPIR.

Clone this wiki locally