Build error

[htzh]

I have the following build error:

File "macro_main.ml", line 1, characters 0-12:
Error: Unbound module Odyl_main

It is probably configuration issue with OMake, but unfortunately I don't know OMake at all. camlp5 is installed and "-I" points to the correct directory.

[ANogin]

I am guessing the version of camlp5 you build did not install odyl_main.cmi / odyl_main.mli into /home/.../.opam/system/lib/camlp5 - you would need to either change tweak the install part of camlp5 build, or copy these two files our of the camlp5 build manually.

[htzh]

Thanks for the response. That moved the build further along (I also needed to copy over odyl_main.cmx, pcaml.cmx and reloc.cmx) till I hit the following:

- build mllib ctime.cmx
+ ocamlopt.opt -warn-error Aez-3-7-29-37-44-45-50 -w Aez-3-7-29-37-44-45-50 -thread -inline 3 -pp ../lib/macropp -I . -I /usr/lib/ocaml/compiler-libs -I ../libmojave/stdlib -I ../libmojave/util -I ../libmojave/unix -c ctime.ml
File "ctime.ml", line 1:
Error: I/O error: /tmp/ocamlpp61f926c2b78539bc920fa76c8b41cbde: File exists
*** omake: 1999/4146 targets are up to date
*** omake: failed (1.97 sec, 0/559 scans, 27/614 rules, 34/445 digests)
*** omake: targets were not rebuilt because of errors:
   mllib/ctime.cmx
      depends on: mllib/ctime.ml
   mllib/ctime.o
      depends on: mllib/ctime.ml

I don't understand the complaint about /tmp/... file exsits. As far as I can tell it doesn't (maybe removed by omake). I am building on ubuntu 18.04 under wsl.

[ANogin]

This is very weird - sounds like a clash in temporary file name... Is this error reproducible if you try building again? Does it still happen with non-parallel (-j1) build?

[htzh]

The tmp file error was repeatable though each time with a different file name. However your suggestion of non-parallel build (-j1) worked and moved me past that hump. After copying over pa_o.cmo and quotation.cmx I was able to get to the following:

- build support/display base_dform.cmoz
+ Shell.prlcomp(lib/camlp5n -o base_dform.ppo base_dform.ml)

----------------------------------
Parse error in entry [con_params], rule:
  [ "["; LIST0 con_param* SEP ","; "]" ]
----------------------------------

File "base_dform.ml", line 204, characters 29-30:              ] 03022 / 04147 While expanding quotation "con":
Parse error: [con_param] expected after '[' (in [con_params])
*** omake: 3025/4147 targets are up to date
*** omake: failed (8.21 sec, 86/667 scans, 60/1362 rules, 171/590 digests)
*** omake: targets were not rebuilt because of errors:
   support/display/base_dform.cmoz
      depends on: support/display/base_dform.ml
   support/display/base_dform.ppo
      depends on: support/display/base_dform.ml

[htzh]

I wonder if this is config related. Omake tried to probe for the browsers during the configuration phase but none was found (I am building under wsl). Maybe there is some feature that I need to turn off.

[ANogin]

I am pretty sure it's not about browsers. What version of ocaml and camlp5 are you using? MetaPRL is very sensitive to that - I believe Jason had updated things to work with 4.05 a couple of years ago, and it's quite likely it would only work with that particular version...

[htzh]

I am on ocaml 4.05 and camlp5 7.06. I did have to add 7.06 to the config file (it topped out at 7.03 which I assumed was what was available back then). If you think the failure may be camlp5 related I can downgrade to camlp5 7.03 and retry.

[htzh]

I tried 7.03 and there is actually regression:

File "infix.ml", line 46, characters 2-21:
Error: Unbound value Grammar.safe_extend
*** omake: 2569/4147 targets are up to date

I checked and Grammar.safe_extend is not in grammar.mli for version 7.03, but it is in the master on github.

[ANogin]

This is the stuff that Jason modified two years ago when he added OCaml 4.05 support - I guess, unless Jason is around to respond to this thread, you will have to figure out yourself which version of camlp5 might work here...

[ANogin]

But wait, where is Grammar.safe_extend coming from? I am seeing Grammar.extend on filter/base/infix.ml:46

[htzh]

Yes that is really weird. Somehow

$ git status
On branch master
Your branch is up to date with 'origin/master'.

Changes not staged for commit:
  (use "git add <file>..." to update what will be committed)
  (use "git checkout -- <file>..." to discard changes in working directory)

        modified:   OMakefile_common
        modified:   filter/base/infix.ml

no changes added to commit (use "git add" and/or "git commit -a")

diff --git a/filter/base/infix.ml b/filter/base/infix.ml
index 4664b6195..72efbc01c 100644
--- a/filter/base/infix.ml
+++ b/filter/base/infix.ml
@@ -43,54 +43,64 @@ let prefix_name op = "prefix_" ^ op
  * Add an infix keyword.
  *)
 let add_infix (keyword : string) =
-  Grammar.extend
+  Grammar.safe_extend
     (let _ = (expr : 'expr Grammar.Entry.e) in
-     [Grammar.Entry.obj (expr : 'expr Grammar.Entry.e),
-      Some (Gramext.Level "expr1"),
-      [Some "expr1", Some Gramext.LeftA,
-       [[Gramext.Sself; Gramext.Stoken ("", keyword); Gramext.Sself],
-        Gramext.action
-          (fun (e2 : 'expr) (op : string) (e1 : 'expr) (_loc : Ploc.t) ->
-             (MLast.ExApp
-                (_loc,
-                 MLast.ExApp
-                   (_loc, MLast.ExLid (_loc, Ploc.VaVal (prefix_name op)),
-                    e1),
-                 e2) :
-              'expr))]]])

Does something in the build process change the source code?! I am certainly incapable of this change.

[ANogin]

Yes, that looks like a bug in Jason's 4.05 change - the file is a generated file and needs to be removed from the repository, added to .gitignore, and added to the clean command in the corresponding OMakefile.

[htzh]

I rechecked out the file so the changes are abandoned and now I am back to about the same place with a similar failure as in 7.06 (slightly further along at 3075 instead of 3025):

- build support/display comment.cmoz
+ Shell.prlcomp(lib/camlp5n -o comment.ppo comment.ml)

----------------------------------
Parse error in entry [con_params], rule:
  [ "["; LIST0 con_param* SEP ","; "]" ]
----------------------------------

File "comment.ml", line 481, characters 33-34:
While expanding quotation "con":
Parse error: [con_param] expected after '[' (in [con_params])
*** omake: 3078/4149 targets are up to date
*** omake: failed (13.67 sec, 118/684 scans, 116/1374 rules, 189/631 digests)
*** omake: targets were not rebuilt because of errors:
   support/display/comment.cmoz
      depends on: support/display/comment.ml
   support/display/comment.ppo
      depends on: support/display/comment.ml

[ANogin]

I do not know enough about camlp5 or Jason's ocaml 4.05 changes to help you further, sorry.

[htzh]

I removed the infix.ml file and regenerated and it is identical to the one checked into the repo (by mistake). So at least I now know that I am using the same version of camlp5 (as I assume it is unlikely for the generated file to be the same otherwise). I also omake clean and omake -j1 and now I get the same error as #1 (comment) so it appears that the minor difference in which file triggers the parse error is an artifact of the build order.

[htzh]

@ANogin Thanks a lot for your help! Do you know if the SVN version still builds with older version of ocaml? This project seems very ambitious but for now I am really just interested in some core ideas used here (the meta logic theory portion). So I would be happy to build a small fragment of it if possible just to see how well the encoded theories work.

[ANogin]

I have not tried it in years, but I would imagine if you had sufficiently old versions of the relevant dependencies, it should work as well as it used to...

[htzh]

If you don't mind me ask: how well did it work? Why was the project abandoned (seems like a lot of effort was put into it)? I understand that main developers could have change in life circumstances but it seems there was not much interest in further development by others at Cornell either? Is nuprl also mostly dead?

[ANogin]

It worked pretty well. Then all major authors/contributors went to work for industry, and it was just left alone to die. OMake almost died as well, and was indeed left largely unmaintained for a number of years, but there were enough fans & users left to keep it alive.

[LdBeth]

I figured that CamlP5 expects user to call mkcamlp5 script to build an executable. Currently I'm working on building with the most recent OCaml 4.11, hope can bring this to alive again.

---

The Nuprl 5 virtual machine image available from Cornell still works pretty well, despite the whole thing is so monstrous that requires an hour booting process to start proving something, so saving a vm snapshot for next use is recommended. The library shipped with the vm image it has many examples of non-trivial theories albeit it is not the latest development.

[ANogin]

A few months ago I got MetaPRL working with a reasonably recent OCaml / Camlp5, but there were a bunch of further fixes that were needed to make this all work. I will see if my employer will allow me to release them (but they do not like doing it and it might take a while :( ).

[LdBeth]

After a day work my current progress on porting to OCaml 4.11 is 3496/4152. No luck get my Perl module work to use mkcamlp5 but by adjust OMakefile the macro preprocessor can be compiled without patching CamlP5 installation.

owo-lang@996cbe0

The major obstacle is that CamlP5 8.00 has made significant amount of undocumented API changes since 7.12 (the latest documented version) that filter_ocaml needs to be revised carefully. The warning levels also needs to be adjusted accordingly to make OCaml compiler happy, but that seems not very difficult.

A few months ago I got MetaPRL working with a reasonably recent OCaml / Camlp5, but there were a bunch of further fixes that were needed to make this all work.

That would be very helpful. fully loaded wishes and looking forward for the next release.

[ANogin]

The versions I got working are:

• OCaml: 4.07.0 4.07.1 4.08.0 4.08.1 4.09.0
• Camlp5: 7.08 7.09 7.10

Going beyond those would likely require extra work.

For camlp5, I also had to make a minor tweak to its own code - removing the "Plexer.dollar_for_antiquotation.val := False" from etc/pa_o.ml (could not figure out how to override this behavior without code change).

[LdBeth]

thank you for the info. I decide to make a branch that uses CamlP5 7.12 since it has been updated to compile with OCaml 4.11, cherry pick some changes I made, and postponed porting to 8.00 until more examples are available.

the antiquotation is related to the "transitional mode" to "strict mode" change of CamlP5, by now 7.12 and later version defaults to strict mode, and it can not be properly switched without recompiling camlp5 according to the manual.

[LdBeth]

This is the change I made on filter_ocaml to make it compatible for 7.12

owo-lang@866c5c0#diff-6716db66faa1b2d725649e375c023cd6R2974

I'm uncertain about the changes I made on line 2967 & 2972, the cause is camlp5 changes

SgMod of loc and V bool and V (list (V string) * module_type))

with added option

SgMod of loc and V bool and V (list (V (option (V string)) * module_type))

but I'm not sure if I should raise a exception when a None is encountered.

fixed in

owo-lang@97a327f

Also there're still pattern-matching is not exhaustive on antiquotation patterns. I think it should be changed to use a _ to catch all other unsupported patterns for easiness.

[LdBeth]

anyway, I proceeded with CamlP5 7.13 because some cmx files needed are however not present in 7.12.

I'm sorta see why Plexer.dollar_for_antiquotation.val := False is needed. MetaPRL uses unexposed interface from CamlP5 which undergoes changes, and thus affects ANTIQUOT behavior in term_grammar.ml. just lots of things needs to be redesign to resist API changes.

---

Now I get MetaPRL compile with OCaml 4.11 and CamlP5 7.13, with the hack above on CamlP5.

https://github.com/owo-lang/metaprl/tree/camlp4-7.12

However I get './mptop' terminated by signal SIGSEGV (Address boundary error)

give flag -debug load shows

... (output elided)
Loading theory Nuprl_jprover.ml
Finished loading Nuprl_jprover
Loading theory Nuprl_run.ml
Finished loading Nuprl_run
Loading theory Mp_top.ml
Loading Mp_top
Loading Shell module
Loaded Shell
Starting main loop
fish: './editor/ml/mp -debug load -cli' terminated by signal SIGSEGV (Address boundary error)

I figured the issue is due to what I did to libmojavewhat OCaml made to String and Bytes that affects the implementation of libmojave's printf function. Obj.magic is the source of all evils :P, and many things in libmojave are actually broken without been witnessed.

[LdBeth]

I guess in new versions of OCaml format type are no longer represented as plain strings internally but some more richer data structures, which is why Obj.magic trick not work well.

https://ocaml.org/meetings/ocaml/2013/proposals/formats-as-gadts.pdf

---

The fix I found is to use string_of_format function to convert the format data to literal string. The abuse of Obj.magic still remains though.

For now the shell top level is working 🎉

[LdBeth]

-1 is not recognized as a int but a int -> int partial application. I'm not sure where is the definition used in mp_top, is it defined in the filter module or from CamlP5?

---

Update: fixed in owo-lang@0abb3b5

[LdBeth]

I investigated a little with the dollar_for_antiquotation problem, it is due to that the current filter module based on pa_o doesn't implement antiquation in the intended way that CamlP5 wants user to do. Later versions of CamlP5 with strict ASTs recommends using q_ast over q_MLast for anqituotation in user syntax, and use meta symbol V to indicate possible occurrence of antiquotes. See http://pauillac.inria.fr/~ddr/camlp5/doc/htmlc/q_ast.html