Hi there, I am trying to compile a bytecode version of coq (to use Drop.
) and didn't succeed. Is it still possible?
./configure -byte-only -profile devel
make
[..]
Error: Don't know how to build
_build/install/default/lib/stublibs/dllbyterun_stubs.so
make[1]: *** [Makefile.common:166: _build/install/default/lib/stublibs/dllbyterun_stubs.so] Error 1
make[1]: Leaving directory '/home/courtieu/coq/byteonly'
make: *** [Makefile.make:122: submake] Error 2
I don't think byte-only still works
cc @Emilio Jesús Gallego Arias
If the option is known not to work anymore, we should remove it. Anyway, this probably deserves a bug report.
I will after @Emilio Jesús Gallego Arias confirms.
So nobody uses Drop anymore?
Honestly I always found the trace mechanism (which is the main interest of Drop) quite useless
For all purposes ocamldebug is better
Well, I am not a big user of Drop but I have found sometime useful to call ocaml code directly from there. Something that to my knowledge is not possible from ocamldebug.
-byte-only was working, but it got broken by the rename byterun -> coqrun, sorry for that, should be easy to fix
tho you don't need to do anything special to use drop; from a clean tree
$ dune exec -- dev/shim/coqbyte-prelude
Coq < Drop.
#
It does not work on my machine. Any idea why?
$ git clean -fx
$ git st -uall
On branch master
Your branch is up to date with 'origin/master'.
nothing to commit, working tree clean
$ dune exec -- dev/shim/coqbyte-prelude
Welcome to Coq 8.15+alpha
Error:
File not found on loadpath : ltac_plugin.cm[ao]
Loadpath: /home/courtieu/coq/byteonly:/home/courtieu/coq/byteonly/_build/default/plugins/ring:/home/courtieu/coq/byteonly/_build/default/plugins/btauto:/home/courtieu/coq/byteonly/_build/default/plugins/ssrmatching:/home/courtieu/coq/byteonly/_build/default/plugins/syntax:/home/courtieu/coq/byteonly/_build/default/plugins/ssrsearch:/home/courtieu/coq/byteonly/_build/default/plugins/ssr:/home/courtieu/coq/byteonly/_build/default/plugins/rtauto:/home/courtieu/coq/byteonly/_build/default/plugins/micromega:/home/courtieu/coq/byteonly/_build/default/plugins/ltac:/home/courtieu/coq/byteonly/_build/default/plugins/cc:/home/courtieu/coq/byteonly/_build/default/plugins/funind:/home/courtieu/coq/byteonly/_build/default/plugins/derive:/home/courtieu/coq/byteonly/_build/default/plugins/extraction:/home/courtieu/coq/byteonly/_build/default/plugins/firstorder:/home/courtieu/coq/byteonly/_build/default/plugins/nsatz
Ouch, indeed there is a bug in the coqbyte rule, it builds the native plugins but not the byte-only ones
OK. I will workaround. Should I fill 2 bug reports? One for removing either removing byte-only or fixing it and the other for coqbyte?
As a workaround you can do dune build dev/dune-dbg
before
Indeed two bugs should work, they seem separate issues
Sorry but when I do dune build dev/dune-dbg
I get Error: Don't know how to build dev/shim/dune-dbg
is it dev/dune-dbg instead?
Yup, or you can just use #14545 if you want
as the debugger is not building all the required plugins I see
Last updated: Oct 13 2024 at 01:02 UTC