Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unbound module Mltop when building from source #5

Open
haansn08 opened this issue Jul 19, 2022 · 1 comment
Open

Unbound module Mltop when building from source #5

haansn08 opened this issue Jul 19, 2022 · 1 comment

Comments

@haansn08
Copy link

I'm trying to build this plugin from source as instructed in https://github.com/uds-psl/CoqTM
I'm on Ubuntu LTS with Coq version 8.11.

I'm getting following error when trying to build from a fresh clone:

$ git clone https://github.com/uds-psl/smpl
Cloning into 'smpl'...
$ cd smpl/
$ git checkout coq-8.11 
Branch 'coq-8.11' set up to track remote branch 'coq-8.11' from 'origin'.
Switched to a new branch 'coq-8.11'
$ make
coq_makefile -f _CoqProject -o Makefile.coq
make -f Makefile.coq all
make[1]: Entering directory '/tmp/smpl'
COQDEP VFILES
COQPP src/smpl.mlg
COQDEP src/smpl_plugin.mlpack
CAMLDEP src/smpl.ml
CAMLOPT -c -for-pack Smpl_plugin src/smpl.ml
File "src/smpl.ml", line 2, characters 8-30:
2 | let _ = Mltop.add_known_module __coq_plugin_name
            ^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module Mltop
make[2]: *** [Makefile.coq:626: src/smpl.cmx] Error 2
make[1]: *** [Makefile.coq:327: all] Error 2
make[1]: Leaving directory '/tmp/smpl'
make: *** [Makefile:8: all] Error 2

What could I do about this?

@haansn08
Copy link
Author

The build seems to work fine with Coq 8.15, ocaml-findlib and ocaml-zarith installed.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant