Ali Caglayan (Apr 28 2022 at 09:44): Ali Caglayan (Apr 28 2022 at 09:44):@Karl Palmskog I see that there is a dune branch for coq-dpdgraph, are there plans for this to be the main branch?
Ali Caglayan (Apr 28 2022 at 09:45):I'm wondering because I am trying to get coq-dpdgraph to compile on a newer OCaml, and it looks like the CI there doesn't test anything higher than 4.06 (which was recently bumped in Coq master).
Ali Caglayan (Apr 28 2022 at 09:46):I would guess that dune would make this easier, but I am wondering if it is also possible to test more recent OCaml versions on that CI.
Karl Palmskog (Apr 28 2022 at 09:46):yes, I plan to do the full Dune build conversion, but the test suite is a nightmare to port
Gaëtan Gilbert (Apr 28 2022 at 09:46):I don't see how dune matters for this
Karl Palmskog (Apr 28 2022 at 09:47):see: https://github.com/coq-community/coq-dpdgraph/tree/coq-master/tests and https://github.com/coq-community/coq-dpdgraph/blob/coq-master/Makefile.in#L132
Karl Palmskog (Apr 28 2022 at 09:47):everything works fine with Dune except that quite a few custom rules are needed to capture the test Make tasks (e.g., coqtop is run manually)
Karl Palmskog (Apr 28 2022 at 09:58):everything should work fine on OCaml 4.13 and beyond, though, regardless of build system
Karl Palmskog (Apr 28 2022 at 09:59):anyway, I would be happy to rebase the dune branch if someone wants to help with the test suite port
Ali Caglayan (Apr 28 2022 at 10:13):@Gaëtan Gilbert The reason "dune matters" is because we need to adapt the makefile to work on different OCaml versions. I don't want to spend time tweaking a makefile if we will switch to dune anyway.
Ali Caglayan (Apr 28 2022 at 10:32):Karl Palmskog said:
everything should work fine on OCaml 4.13 and beyond, though, regardless of build system
I was running into issues with mli files being needed.
Karl Palmskog (Apr 28 2022 at 10:32):but then you aren't using Coq from opam?
Karl Palmskog (Apr 28 2022 at 10:33):I think this problem was patched in Coq-on-opam so shouldn't occur for plugins.
Karl Palmskog (Apr 28 2022 at 10:34): Ali Caglayan (Apr 28 2022 at 10:37):Ah I see
Ali Caglayan (Apr 28 2022 at 10:38):Well I was trying to build coq-dpdgraph locally to see what needed to be tweaked to work on newer OCaml
Ali Caglayan (Apr 28 2022 at 10:40):coq-dpdgraph is failing in the HoTT CI after a version bump
Ali Caglayan (Apr 28 2022 at 10:40):https://github.com/HoTT/HoTT/runs/6201957053?check_suite_focus=true#step:6:2509
Karl Palmskog (Apr 28 2022 at 10:41):Unknown option -generate-meta-for-package
This indicates the Coq version is mismatched with the coq-dpdgraph version (the former is too old)
Ali Caglayan (Apr 28 2022 at 10:41):Perhaps I didn't bump the commit properly then
Ali Caglayan (Apr 28 2022 at 10:41):OK that is my stupidity
Ali Caglayan (Apr 28 2022 at 10:41):However on another note, I do have things to generate rules for coqtop
Ali Caglayan (Apr 28 2022 at 10:42):I wrote some rule generation code when porting the test-suite of Coq, but I can easily adapt a few things here and there.
Karl Palmskog (Apr 28 2022 at 10:43):OK, I'll rebase the Dune branch then, feel free to make any improvements you want there (I think you are already a coq-community GitHub member?)
Ali Caglayan (Apr 28 2022 at 10:44):I don't think I am
Karl Palmskog (Apr 28 2022 at 10:45):OK, invite sent. We are quite generous with permissions, so use wisely (coordinate with Coq-community maintainers before merges, etc.)
Karl Palmskog (Apr 28 2022 at 10:46):Théo and I can intervene when a maintainer is not responsive
Ali Caglayan (Apr 28 2022 at 10:47):Ah you mean I can push directly to the branches?
Ali Caglayan (Apr 28 2022 at 10:49):I'll continue to make PRs and merge those instead I think, since pushing directly is a bit dangerous in your muscle memory.
Karl Palmskog (Apr 28 2022 at 10:50):yes, we frown on pushes to master by others than the maintainer. But it may be good to create topic branches directly in the repo (easier for others to take over them and finish stalled PRs)
Ali Caglayan (Apr 28 2022 at 10:59):Actually I am even more confused than before regarding this error in HoTT
Ali Caglayan (Apr 28 2022 at 10:59):I actually patched dpd-graph to ignore warning 70
Ali Caglayan (Apr 28 2022 at 11:00):but the issue seems to stem from the Make file passing this option -generate-meta-for-package coq-dpdgraph
Ali Caglayan (Apr 28 2022 at 11:00):Which coq_makefile doesn't understand
Ali Caglayan (Apr 28 2022 at 11:01):AFAICT this is on top of the latest coq-master branch of dpdgraph
Ali Caglayan (Apr 28 2022 at 11:02):Ah but we are 8.15.1
Karl Palmskog (Apr 28 2022 at 11:02):coq_makefile only understands this command on Coq versions after 8.15
Karl Palmskog (Apr 28 2022 at 11:02):you should use this branch for 8.15: https://github.com/coq-community/coq-dpdgraph/tree/coq-v8.15
Karl Palmskog (Apr 28 2022 at 11:03):or even better, coq-dpdgraph.1.0+8.15 from the released opam repo
Karl Palmskog (Apr 28 2022 at 11:04):for Coq versions after 8.15, I recommend coq-dpdgraph.dev from the extra-dev repo
Karl Palmskog (Apr 28 2022 at 11:05):I rebased this now if you want to try porting the test suite: https://github.com/coq-community/coq-dpdgraph/pull/89
Karl Palmskog (Apr 28 2022 at 11:07):my opinion is that the warning 70 problem should only be dealt with in Coq itself (Coq should silence it for any plugins like coq-dpdgraph)
Ali Caglayan (Apr 28 2022 at 11:08):We have been vendoring dpdgraph as a git submodule for quite some time, I will look into if we can replace it completely using the opam package
Ali Caglayan (Apr 28 2022 at 14:18):That seems to have worked in HoTT
Ali Caglayan (Apr 28 2022 at 14:19):Regarding the tests, I had a look, we don't need any of the rule generation stuff that I was talking about before.
Ali Caglayan (Apr 28 2022 at 14:19):I am fairly sure dune's cram testing will be enough
Ali Caglayan (Apr 28 2022 at 14:19):I will work on it today
Ali Caglayan (Apr 28 2022 at 20:13):I've converted all the tests to cram: https://github.com/coq-community/coq-dpdgraph/pull/101 cc @Karl Palmskog
Paolo Giarrusso (Apr 29 2022 at 02:37):That’s a very cool example of cram tests, they seem great!
Paolo Giarrusso (Apr 29 2022 at 02:38):They even support keeping separate source folders: https://dune.readthedocs.io/en/stable/tests.html#directory-tests! What you did is good, but directory tests could ease actual development on the test sources.
Paolo Giarrusso (Apr 29 2022 at 02:39):(The new dune coq top might work on generated sources, I forget how the discussion ended, but syntax highlighting probably won’t).
Paolo Giarrusso (Apr 29 2022 at 02:41):(And to be clear, I’m not developing on dpdgraph; this is really a digression on using cram tests more broadly in the Coq ecosystem.)
Bas Spitters (Jun 14 2022 at 14:55):@Ali Caglayan I guess it makes sense to generalize the HoTT dpd-graph bash scripts to be rolled out over many coq-community projects.
Would that be feasible with the current setup?
Karl Palmskog (Jun 14 2022 at 14:57):I think it would be best to first fix the problem in dpdgraph that names are not given with absolute paths, e.g., My.Lib.Constant is typically outputted as Lib.Constant or Constant. It seems Ali and I have separate hacks to fix this
Ali Caglayan (Jun 14 2022 at 15:34):I think that can probably be fixed easily, I was not aware of the issue. The hack in the Hott library is not mine, but probably @Jason Gross's.
Ali Caglayan (Jun 14 2022 at 15:35):I can have a look into making more general setups for dpdgraph, since it is an alternative documentation method that might be good to support in say Dune.
Karl Palmskog (Jun 14 2022 at 15:46):here is how I implemented it (full names):
This is to enable linking to coqdoc, i.e., it gives the same name format as coqdoc HTML file names.
Last updated: Apr 19 2024 at 17:02 UTC