Skip to content

Home

Jump to bottom
LdBeth edited this page Apr 16, 2021 · 70 revisions

Welcome to the metaprl wiki!

Progress on porting

The main branch works with OCaml 4.11 and CamlP5 7.13 for 7.12 lacks cmx version of some files.

The camlp5-8.00 works with OCaml 4.11 and CamlP5 e0fa35f for the CamlP-8.00 release has a bug.

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.
  • tear apart the repo so the theories go to a separate one.
  • fix NOTHING handling in pa_macro. now SIMPLE refiner can be chosen.
  • refactored spell checker
  • fixed ifthenelseT
  • Now comments and summary items are not save in prla/prlb files.
  • base file compression
  • port to camlp5-8.00 is almost done.
  • added readline completion

WIP

  • figuring out the various algorithms used for proving.
  • http server sometimes SIGSEGV, it seems to be caused by random dirty bytes read by the server. This could also be lm_ssl.c not cooperating with GC.
  • rewrite to more "idiomatic" OCaml code.
  • The Lm_splay_linear_set has some bug when splay on lazy/offset values. Consider either rewrite it or design a new one.
  • implement term comments. update .prla files accordingly.

HIGH PIRO

  1. make the first release with CamlP5 8.00 integration.

LOW PIOR

  1. improving the browser interface, need someone good at HTTP server programming, web design.
  2. Find a way to test MathBus connection.
  3. Improving mprun, the OCaml repl, figuring out how Shell_p4 work with the toplevel.
  4. Libmojave's MakePrintf haven't been used much in MetaPRL, maybe should just consider remove it.
  5. Improving performance of Lm_rformat, or replace it with something capable pretty print MetaPRL's stuff.
  6. The TERMS_std implementation mismatches the ds version. (SIGSEGV occurs if the cache files are not cleaned up). Mostly address related issues such as find_subterm etc. moved to low priority because majority of proofs are not yet affected.
  7. Print proof terms like Nuprl, that only the changed assumptions are displayed in subgoals. This should be implemented in Proof_edit module.

TODO

  • Add fuzzy matching for cd, so one can write liFor2 for listFormation2 in the REPL.
  • Add registry for jumping between recently viewed proof nodes.
  • continue to develop LF theory.
  • use ocamlfind for dependency management.
  • currently, theories cannot be displayed if they are not sub theories of Shell. Try improve this mechanism. Maybe just hide them.
  • the result byte code toplevel 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.

    • The list type was once a primitive in Nuprl. Later, it was defined using the "Mendler" fixpoint type. Now we define lists as those "co-lists" for which the length (a partially defined function) has a value. Once we show that the list iterator is well formed (see list_ind_wf) then we can use list as an abstract type. This "implementation" shows that we only need induction on Nat to build lists, and do not need the power of the Mendler fixpoint or a general inductive construction.

  • add definition resource so unfoldT foldT can be used instead of directly call convs, and implement NuPRL style RWW accordingly.
  • fix the "derived" rule/rw function.
  • soft abstraction, which should be easy with the resource mechanism.
  • redesign the code listing, what I want is actually something resembles WEB.
  • Port Coqrewrite to MetaPRL, design a way to emulate typeclass.

flambda

Please don't use flambda, it is currently incompatible due to cross module optimization not working 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

Port to 8.00 is almost done. The only extra file needed to copy is odyl/odyl_main, however this should be fixed soon.

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. (with the --safe-string thing disabled). However, MetaPRL uses a very old version of ensemble, so the server program needs to be rewritten. It might be possible to use Multicore OCaml as a candidate for multiple threads refiner.

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.

LZ4

Experimental support for compressing theory files.

Clone this wiki locally