Stream: Coq devs & plugin devs

Topic: Bytecode build


view this post on Zulip Pierre Courtieu (Jun 23 2021 at 10:03):

Hi there, I am trying to compile a bytecode version of coq (to use Drop.) and didn't succeed. Is it still possible?

view this post on Zulip Pierre Courtieu (Jun 23 2021 at 10:14):

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

view this post on Zulip Gaëtan Gilbert (Jun 23 2021 at 10:17):

I don't think byte-only still works
cc @Emilio Jesús Gallego Arias

view this post on Zulip Théo Zimmermann (Jun 23 2021 at 10:24):

If the option is known not to work anymore, we should remove it. Anyway, this probably deserves a bug report.

view this post on Zulip Pierre Courtieu (Jun 23 2021 at 11:09):

I will after @Emilio Jesús Gallego Arias confirms.
So nobody uses Drop anymore?

view this post on Zulip Pierre-Marie Pédrot (Jun 23 2021 at 11:46):

Honestly I always found the trace mechanism (which is the main interest of Drop) quite useless

view this post on Zulip Pierre-Marie Pédrot (Jun 23 2021 at 11:46):

For all purposes ocamldebug is better

view this post on Zulip Pierre Courtieu (Jun 23 2021 at 13:00):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2021 at 13:21):

-byte-only was working, but it got broken by the rename byterun -> coqrun, sorry for that, should be easy to fix

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2021 at 13:21):

tho you don't need to do anything special to use drop; from a clean tree

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2021 at 13:21):

$ dune exec -- dev/shim/coqbyte-prelude
Coq < Drop.
#

view this post on Zulip Pierre Courtieu (Jun 23 2021 at 15:32):

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

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2021 at 15:35):

Ouch, indeed there is a bug in the coqbyte rule, it builds the native plugins but not the byte-only ones

view this post on Zulip Pierre Courtieu (Jun 23 2021 at 15:47):

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?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2021 at 15:49):

As a workaround you can do dune build dev/dune-dbg before

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2021 at 15:50):

Indeed two bugs should work, they seem separate issues

view this post on Zulip Pierre Courtieu (Jun 23 2021 at 18:24):

Sorry but when I do dune build dev/dune-dbg I get Error: Don't know how to build dev/shim/dune-dbg

view this post on Zulip Pierre Courtieu (Jun 23 2021 at 18:26):

is it dev/dune-dbg instead?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2021 at 18:32):

Yup, or you can just use #14545 if you want

view this post on Zulip Emilio Jesús Gallego Arias (Jun 23 2021 at 18:32):

as the debugger is not building all the required plugins I see


Last updated: Oct 13 2024 at 01:02 UTC