Matthieu Sozeau (Oct 09 2024 at 11:12): Matthieu Sozeau (Oct 09 2024 at 11:12):Gaëtan Gilbert said:
there are some files which seem to depend on hott but don't work
you can see in the bench logs https://coq.gitlabpages.inria.fr/-/coq/-/jobs/4796843/artifacts/_bench/logs/coq-equations.NEW.opam_install.1.stdout.log- COQC theories/HoTT/Classes.v - File "./theories/HoTT/Classes.v", line 11, characters 33-42: - Error: Cannot find a physical path bound to logical path HoTT.HSet.(the bench does install hott before equations)
I don't do Equations + HoTT CIs often enough to catch these... but this should not be a problem if we move to the repo, there can be an out-of-rocq-repo equations-hott variant that just installs the extension .v files
Matthieu Sozeau (Oct 09 2024 at 11:14):We discussed moving Equations to the main repo a bit. I think it's easily doable. The second step will be to integrate it with the rest of Gallina/tactics which is more long term work but could be beneficial (e.g. using dependent induction by default, noconfusion and the like)
Matthieu Sozeau (Oct 09 2024 at 11:15):Equations does not really depend on the stdlib, it just needs a prelude (with equality and sigma type being defined basically)
Ali Caglayan (Oct 09 2024 at 11:16):Are you just using Register in the HoTT equations? In that case, it might make sense in its own repo/project depending on both equations and HoTT and then just rocq and hott
Matthieu Sozeau (Oct 09 2024 at 11:16):I'm using Register for everything indeed
Enrico Tassi (Oct 09 2024 at 11:31):I think generating noconfusion (and a bunch of other stuff) is a bit orthogonal to Equations. Since equation needs it, and since Coq does not provide a synthesis for it, it made sense to have it there but, IMO, it should be split and merged/hooked in first.
IMHO this kind of work is better placed in the context of improving (the lower layers of) a standard library. Also I'd first implement namespaces in the core, then the support to hook-in derivations, and then put effort in such a rework of the stdlib using the new features. But that is a longer discussion...
I don't know very well the code base of Equations, so I can't evaluate the immediate benefit of merging it. Maybe they are considerable. If they are not, I'd rather work out a more precise plan first.
Notification Bot (Oct 09 2024 at 11:32):18 messages were moved here from #Coq devs & plugin devs > coq call by Théo Zimmermann.
Guillaume Melquiond (Oct 09 2024 at 12:11):Matthieu Sozeau said:
Equations does not really depend on the stdlib, it just needs a prelude (with equality and sigma type being defined basically)
That is more than just a prelude:
From Stdlib Require Import Wf_nat Relations.
From Stdlib Require Import Wellfounded Relation_Definitions.
From Stdlib Require Import Relation_Operators Lexicographic_Product Wf_nat.
From Stdlib Require Export Program.Wf FunctionalExtensionality.
Require Import Bvector List.
Require Import Extraction CRelationClasses.
Right, there's WF relations as well, but program needs those as well. Bvector and List are not strictly necessary for sure
Matthieu Sozeau (Oct 09 2024 at 12:32):NoConfusion for dependent inductive types requires in general the whole equations compiler, so it's a bit all-or-nothing :)
Guillaume Melquiond (Oct 09 2024 at 13:07):Matthieu Sozeau said:
Right, there's WF relations as well, but program needs those as well.
Sure, but Program is being removed from the main repository (https://github.com/coq/coq/pull/19530/commits/5a269b7b608ac07347fe0e4097eda8b52c8fa093). That is why I am saying that it will be difficult to move Equations into the main repository.
Gaëtan Gilbert (Oct 09 2024 at 13:08):Program.Wf doesn't seem to be touched in that commit
Gaëtan Gilbert (Oct 09 2024 at 13:11):also if the split turns out to be a significant obstacle to development we can just say experiment successfully failed
Emilio Jesús Gallego Arias (Oct 09 2024 at 13:30):Pierre Roux said:
Sorry, I don't feel qualified here (maybe I'm not using parallelism enough myself but I never encountered that kind of issues). If the change of behavior is not consensual, couldn't you just add an option whose default would be the current behavior and explicitly activate the behavior you want in dune? That could be more consensual, and we could still change the default later when a consensus is reached.
This is not about dune, but about coqdep.
Last updated: Oct 13 2024 at 01:02 UTC