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: *** [Makefile.common:166: _build/install/default/lib/stublibs/dllbyterun_stubs.so] Error 1 make: 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: Jun 04 2023 at 19:30 UTC