Emilio Jesús Gallego Arias (May 25 2022 at 15:12): Emilio Jesús Gallego Arias (May 25 2022 at 15:12):@Ali Caglayan points out that there are some problems when using Coq and Dune in newer Coq versions. I didn't check for 8.16, but for 8.15, the Dune Coq language test suite runs well, so I can't detect any problem. Can you provide a reproduction case here?
Ali Caglayan (May 25 2022 at 15:18):dune build will work.
Do a dune clean.
dune build --cache=disabled theories/UsingMyPlugin.vo and it doesn't.
Ali Caglayan (May 25 2022 at 15:22):Same with this.
Emilio Jesús Gallego Arias (May 25 2022 at 15:23):Which Coq version?
Ali Caglayan (May 25 2022 at 15:23):8.16
Emilio Jesús Gallego Arias (May 25 2022 at 15:23):ok let me see
Ali Caglayan (May 25 2022 at 15:25):In 8.15, once you modify to the legacy names they work
Ali Caglayan (May 25 2022 at 15:26):I believe the crux of the problem is that the dune rules don't rely on the META file.
Emilio Jesús Gallego Arias (May 25 2022 at 15:34):Oh, the problem is that Dune doesn't support that method
Emilio Jesús Gallego Arias (May 25 2022 at 15:34):at all indeed
Emilio Jesús Gallego Arias (May 25 2022 at 15:35):you need to use
Emilio Jesús Gallego Arias (May 25 2022 at 15:35):Declare ML Module "MyPlugin".
Emilio Jesús Gallego Arias (May 25 2022 at 15:37):It should be like this Declare ML Module "my_plugin:my-coq-plugin.plugin".
Emilio Jesús Gallego Arias (May 25 2022 at 15:38):The new form is just not supported, the one I propose likely has a bug
Emilio Jesús Gallego Arias (May 25 2022 at 15:38):So indeed we need to document that.
Emilio Jesús Gallego Arias (May 25 2022 at 15:47):Yes master works fine for me
Emilio Jesús Gallego Arias (May 25 2022 at 15:47):great job by Enrico keeping the compat
Emilio Jesús Gallego Arias (May 25 2022 at 15:47):Actually my PR makes it fail, but the fix is easy
Emilio Jesús Gallego Arias (May 25 2022 at 15:52):Dune's test-suite works fine in master !
Emilio Jesús Gallego Arias (May 25 2022 at 15:52):Provided we adapt the test cases to the new declare ML syntax
Emilio Jesús Gallego Arias (May 25 2022 at 15:55):So @Ali Caglayan , does that solve your problem?
Ali Caglayan (May 25 2022 at 16:00):@Emilio Jesús Gallego Arias Are you running the tests correctly? dune build @test/blackbox-tests/test-cases/coq/runtest?
Ali Caglayan (May 25 2022 at 16:01):Also make sure you have a more recent version of dune or else dune skips the coq tests when coq is not present
Emilio Jesús Gallego Arias (May 25 2022 at 16:04):I think I'm running the tests correctly
Emilio Jesús Gallego Arias (May 25 2022 at 16:05):I'm using Dune master plus Coq master
Emilio Jesús Gallego Arias (May 25 2022 at 16:05):and this PR
Emilio Jesús Gallego Arias (May 25 2022 at 16:05):https://github.com/ocaml/dune/pull/5776
Emilio Jesús Gallego Arias (May 25 2022 at 16:11):So actually things work fine with my PR, @Ali Caglayan you have another bug in your code
Emilio Jesús Gallego Arias (May 25 2022 at 16:12):the mlg should have DECLARE PLUGIN "my-coq-plugin.plugin"
Ali Caglayan (May 25 2022 at 16:18):Why does it work the other way?
Emilio Jesús Gallego Arias (May 25 2022 at 16:19):What do you mean @Ali Caglayan ?
Ali Caglayan (May 25 2022 at 16:19):Emilio Jesús Gallego Arias said:
the mlg should have
DECLARE PLUGIN "my-coq-plugin.plugin"
Why?
Emilio Jesús Gallego Arias (May 25 2022 at 16:19):Oh because the table that checks required plugins is using the new plugin name as index
Ali Caglayan (May 25 2022 at 16:19):It also worked when it was wrong so I am confused about the point of this.
Emilio Jesús Gallego Arias (May 25 2022 at 16:19):not after my PR, that was a bug in old code
Emilio Jesús Gallego Arias (May 25 2022 at 16:20):it was too loose
Emilio Jesús Gallego Arias (May 25 2022 at 16:20):and registered the wrong name
Ali Caglayan (May 25 2022 at 16:20):Does it still work when you target a vo from a clean build?
Emilio Jesús Gallego Arias (May 25 2022 at 16:20):then it needed the hack, now we use the findlib name all the time
Emilio Jesús Gallego Arias (May 25 2022 at 16:21):yes it works for me, please test!
Emilio Jesús Gallego Arias (May 25 2022 at 16:22):So migration is basically to replace the old names
Emilio Jesús Gallego Arias (May 25 2022 at 16:22):and in dune we need to use the foo:pkg.foo syntax
Emilio Jesús Gallego Arias (May 25 2022 at 16:22):for now
Emilio Jesús Gallego Arias (May 25 2022 at 16:48):Does it work for you ?
Ali Caglayan (May 25 2022 at 17:04):Looks like it
Ali Caglayan (May 25 2022 at 17:04):Thanks for documenting it in the mltop PR
Emilio Jesús Gallego Arias (May 25 2022 at 17:06):I just learned how it works lol
Emilio Jesús Gallego Arias (May 25 2022 at 17:06):I mean a couple of days ago
Emilio Jesús Gallego Arias (May 25 2022 at 17:06):but it looks good to me
Emilio Jesús Gallego Arias (May 25 2022 at 17:06):now we need to fix (coq.theory ...)
Emilio Jesús Gallego Arias (May 25 2022 at 17:07):that'll be easy, I think we have been making things more complex than they are
Emilio Jesús Gallego Arias (May 25 2022 at 17:12):but build stuff is tricky one needs a lot of discipline, specially with a system like dune which is so precise
Last updated: Apr 16 2024 at 19:01 UTC