Skip to content
This repository has been archived by the owner on Nov 7, 2020. It is now read-only.
LdBeth edited this page Sep 23, 2020 · 42 revisions

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. various compatibility issues: http server sometimes SIGSEGV
  2. Get to understand new CamlP5 8.00 API, finish migration.
  3. Working with CamlP5 developers for filter module porting.

LOW PIOR

  1. 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.

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 for a long period. Bring back this feature might also require reviving the Ensemble code.

Clone this wiki locally