Stream: coq-community devs & users

Topic: dpd-graph


view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Apr 28 2022 at 09:46):

I don't see how dune matters for this

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Karl Palmskog (Apr 28 2022 at 09:58):

everything should work fine on OCaml 4.13 and beyond, though, regardless of build system

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Apr 28 2022 at 10:32):

but then you aren't using Coq from opam?

view this post on Zulip Karl Palmskog (Apr 28 2022 at 10:33):

I think this problem was patched in Coq-on-opam so shouldn't occur for plugins.

view this post on Zulip Karl Palmskog (Apr 28 2022 at 10:34):

example: https://github.com/ocaml/opam-repository/blob/master/packages/coq/coq.8.13.2/files/disable_warn_70.patch

view this post on Zulip Ali Caglayan (Apr 28 2022 at 10:37):

Ah I see

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Apr 28 2022 at 10:40):

coq-dpdgraph is failing in the HoTT CI after a version bump

view this post on Zulip Ali Caglayan (Apr 28 2022 at 10:40):

https://github.com/HoTT/HoTT/runs/6201957053?check_suite_focus=true#step:6:2509

view this post on Zulip 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)

view this post on Zulip Ali Caglayan (Apr 28 2022 at 10:41):

Perhaps I didn't bump the commit properly then

view this post on Zulip Ali Caglayan (Apr 28 2022 at 10:41):

OK that is my stupidity

view this post on Zulip Ali Caglayan (Apr 28 2022 at 10:41):

However on another note, I do have things to generate rules for coqtop

view this post on Zulip 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.

view this post on Zulip 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?)

view this post on Zulip Ali Caglayan (Apr 28 2022 at 10:44):

I don't think I am

view this post on Zulip 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.)

view this post on Zulip Karl Palmskog (Apr 28 2022 at 10:46):

Théo and I can intervene when a maintainer is not responsive

view this post on Zulip Ali Caglayan (Apr 28 2022 at 10:47):

Ah you mean I can push directly to the branches?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Ali Caglayan (Apr 28 2022 at 10:59):

Actually I am even more confused than before regarding this error in HoTT

view this post on Zulip Ali Caglayan (Apr 28 2022 at 10:59):

I actually patched dpd-graph to ignore warning 70

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Apr 28 2022 at 11:00):

Which coq_makefile doesn't understand

view this post on Zulip Ali Caglayan (Apr 28 2022 at 11:01):

AFAICT this is on top of the latest coq-master branch of dpdgraph

view this post on Zulip Ali Caglayan (Apr 28 2022 at 11:02):

Ah but we are 8.15.1

view this post on Zulip Karl Palmskog (Apr 28 2022 at 11:02):

coq_makefile only understands this command on Coq versions after 8.15

view this post on Zulip 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

view this post on Zulip Karl Palmskog (Apr 28 2022 at 11:03):

or even better, coq-dpdgraph.1.0+8.15 from the released opam repo

view this post on Zulip Karl Palmskog (Apr 28 2022 at 11:04):

for Coq versions after 8.15, I recommend coq-dpdgraph.dev from the extra-dev repo

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Apr 28 2022 at 14:18):

That seems to have worked in HoTT

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 28 2022 at 14:19):

I am fairly sure dune's cram testing will be enough

view this post on Zulip Ali Caglayan (Apr 28 2022 at 14:19):

I will work on it today

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Apr 29 2022 at 02:37):

That’s a very cool example of cram tests, they seem great!

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Feb 05 2023 at 15:03 UTC