Jonathan Cubides (Oct 15 2020 at 19:55): Jonathan Cubides (Oct 15 2020 at 19:55):I had also error checking the code from: https://github.com/coq-contribs/jordan-curve-theorem.
I got this error:
make
make -f Makefile.coq Makefile
COQDEP VFILES
make[1]: Nothing to be done for `Makefile'.
make -f Makefile.coq all
COQC Jordan1.v
File "./theories/Init/Tauto.v", line 101, characters 14-68:
Error: Tactic failure: Classical tauto failed.
make[2]: *** [Jordan1.vo] Error 1
make[1]: *** [all] Error 2
make: *** [all] Error 2
Should I do something about it? I don't have any idea how to fix it. This and the previous repo are a bit old.
Is that maybe also running in Coq 8.10?
Paolo Giarrusso (Oct 15 2020 at 20:03):That code is much older, since 8.10 is from 2019
Paolo Giarrusso (Oct 15 2020 at 20:03):(https://github.com/coq/coq/releases/tag/V8.10.0)
Paolo Giarrusso (Oct 15 2020 at 20:05):The latest release back then was 8.4pl5 https://github.com/coq/coq/releases?after=V8.5rc1
Paolo Giarrusso (Oct 15 2020 at 20:06):the authors might have used an older Coq, but hopefully not (that'd be mean)
Paolo Giarrusso (Oct 15 2020 at 20:07):I doubt such old Coq versions support VsCoq, coqide and emacs are the likely options.
Jonathan Cubides (Oct 15 2020 at 20:11):I can work with emacs, it's not a problem. Do you know any docker with that Coq version? I'll investigate on that. Maybe that's much easier. Idk.
Anton Trunov (Oct 15 2020 at 20:12):@Jonathan Cubides You can find a lot of Docker images here: https://hub.docker.com/r/coqorg/coq
Anton Trunov (Oct 15 2020 at 20:13):8.4 is there
Karl Palmskog (Oct 15 2020 at 23:00):huh? Jordan curve project works fine with Coq 8.10 (v8.10.0 branch of the project), why on earth go back to 8.4? I can step through the project just fine in VsCode. Coq 8.10 was released just one year ago
Karl Palmskog (Oct 15 2020 at 23:03):to get "full" VsCode support, one must copy Make to _CoqProject though
Paolo Giarrusso (Oct 16 2020 at 00:17):Well, does https://github.com/coq-contribs/jordan-curve-theorem say that? The default branch is master, whose last commit is from 2016, and which mentions no version information in the README.
Karl Palmskog (Oct 16 2020 at 00:18):where does it say that master is the latest version for contribs generally?
Paolo Giarrusso (Oct 16 2020 at 00:19):it's the default branch. GitHub lets you change that.
Karl Palmskog (Oct 16 2020 at 00:20):contribs were maintained a certain way, long before the move to GitHub. The version of Coq supported is indicated by the available tags
Paolo Giarrusso (Oct 16 2020 at 00:21):Well, so after the move there's a usability/discoverability bug.
Karl Palmskog (Oct 16 2020 at 00:22):have you read this part about contribs generally? https://github.com/coq-community/manifesto#faq
Karl Palmskog (Oct 16 2020 at 00:23):bottom line: contribs are legacy, maintained at the personal discretion of some of the Coq devs and contributors
Paolo Giarrusso (Oct 16 2020 at 00:24):well, I haven't said that somebody has to fix it
Paolo Giarrusso (Oct 16 2020 at 00:25):and I should say: thanks for suggesting a better solution!
Paolo Giarrusso (Oct 16 2020 at 00:26):but to the "why on Earth...", it's because the correct solution was not discoverable enough.
Karl Palmskog (Oct 16 2020 at 00:26):the framing is basically: contribs are known to be a ghost town. If one of the houses has a defective window, to call this a "building bug" is stretching the meaning of bug
Paolo Giarrusso (Oct 16 2020 at 00:27):bug != somebody must fix it
Paolo Giarrusso (Oct 16 2020 at 00:28):especially for usability bugs, it's tons of work
Karl Palmskog (Oct 16 2020 at 00:29):if you don't have a spec for something, how can it be a bug? The usual thing to do in software engineering is to call it a "surprise"
Shea Levy (Oct 16 2020 at 00:30):Karl Palmskog said:
if you don't have a spec for something, how can it be a bug? The usual thing to do in software engineering is to call it a "surprise"
Notions of correct and incorrect behavior come well before specs...
Paolo Giarrusso (Oct 16 2020 at 00:30):I'm not sure this debate is useful, but to me GitHub does imply a spec.
Paolo Giarrusso (Oct 16 2020 at 00:31):Focusing on "actionable things", GitHub _allows_ marking "ghost town" by archiving them, tho nobody _has_ to.
Paolo Giarrusso (Oct 16 2020 at 00:32):I apologize for trying to solve the problem without knowing the correct answer — let me know if I shouldn't :-).
Paolo Giarrusso (Oct 16 2020 at 00:33):and I apologize for reacting to "why on Earth" by actually answering that question — that was not productive.
Karl Palmskog (Oct 16 2020 at 00:34):I said "why on earth" because I couldn't figure out what the connection to 8.4 was. Basically, the master branch works on many versions of Coq after 8.4
Paolo Giarrusso (Oct 16 2020 at 00:37):Ah well, I only saw a README naming no Coq version, omitted the relevant rant, then found the latest Coq release at the time.
Karl Palmskog (Oct 16 2020 at 00:39):I think there are many projects on GitHub that should not be archived (since someone is still updating them on a when-possible basis), and unfortunately, they are completely caveat emptor (buyer beware). I would not be surprised if most GitHub projects are like this.
Paolo Giarrusso (Oct 16 2020 at 00:40):Anyway, at least Coq-community projects do list supported Coq versions https://github.com/coq-community/hoare-tut#meta :-). That's cool.
Paolo Giarrusso (Oct 16 2020 at 00:41):And next time, if I remember, I'll check branches and tags.
Karl Palmskog (Oct 16 2020 at 00:43):sounds good. Unfortunately, the best response to anyone who is not an experienced Coq user who is trying out contribs is: it is very likely you will want to look elsewhere for projects
Karl Palmskog (Oct 16 2020 at 00:44):the contribs are immensely valuable for researchers though, they contain almost every Coq development described in research publications from maybe 1998 to 2014 or so
Théo Zimmermann (Oct 16 2020 at 12:21):Well, actually if some user is particularly interested in one given contrib, I would encourage them to propose to maintain it as part of coq-community.
Théo Zimmermann (Oct 16 2020 at 12:21):(like we have successfully done many times in the past)
Théo Zimmermann (Oct 16 2020 at 12:23):Besides, given that the only developer left maintaining contribs is @Hugo Herbelin, I'd like to know the list of the ones that are definitely unmaintained so that we can update their README with this information and also a link to coq-community in case someone wants to revive them.
Karl Palmskog (Oct 16 2020 at 12:29):I have been known to make some pushes to contribs when we improved them in research, but I try not to get in Hugo's way. Knowing which ones are not feasible to update would be interesting.
Hugo Herbelin (Oct 16 2020 at 19:37):The contribs that I definitely renounced to maintain already have a README with this information. This is the case of legacy-ring which is entirely subsumed and has no reason to be maintained (and similarly for
legacy-field, jprover, rational).
Among the ones that are difficult to maintain but I believe are valuable, there are counting, nfix and the certified SMT ergo, though I lost track of what exists regarding SMT (the main difficulties are the changes in the tactic API).
I promised to port relation-extraction which Catherine Dubois wants to maintain (but I currently stopped at supporting 8.10, [ADDED:] starting from a different branch by Pierre-Nicolas Tollitte).
Those without ML code are relatively easy to maintain, to the exception of:
algebra and what depends on it: LinAlg and orbstab: too many issues with the change of import of coercions. Note that someone said they wanted to look at it. I don't know if there was a conclusionhigh-school-geometry: too many problems with the change of representation of real constants. It is a pity because this was a nice experiment of using a proof assistant in a high schoolSome other failures, in classical-realizability and bdds are probably not so difficult to fix. For area-method, we need a replacement to Quote. I find descente-infinie cool and maple worth more advertising but their ML parts need a fix.
This is what I can tell from my archive. Maybe some people have worked on them independently, I don't know. In any case, I don't feel proprietary of them, so no worry if you find a maintainer for them.
Karl Palmskog (Oct 16 2020 at 21:59):high-school-geometry is maintained now in coq-community, we have marked the contrib repo as archived and have a link to the new location: https://github.com/coq-contribs/high-school-geometry
Karl Palmskog (Oct 16 2020 at 22:01):for legacy-ring, I think we can go ahead and mark it as archived and link to the upstream ring tactic documentation? https://coq.inria.fr/distrib/current/refman/addendum/ring.html
Karl Palmskog (Oct 16 2020 at 22:12):same for legacy-field and rational
Karl Palmskog (Oct 16 2020 at 22:40):for relation-extraction, see https://github.com/coq-community/manifesto/issues/25 - best would be if a new maintainer commented on this issue
Karl Palmskog (Oct 16 2020 at 22:42):since archiving is reversible, I'm going to mark legacy-ring, legacy-field, and rational right away
Hugo Herbelin (Oct 17 2020 at 09:41):Karl Palmskog said:
high-school-geometryis maintained now in coq-community, we have marked the contrib repo as archived and have a link to the new location: https://github.com/coq-contribs/high-school-geometry
Great, then I removed it from the list of coq-contribs submodules.
since archiving is reversible, I'm going to mark legacy-ring, legacy-field, and rational right away
I did not know about this step. Thanks!
for relation-extraction, see https://github.com/coq-community/manifesto/issues/25 - best would be if a new maintainer commented on this issue
Done
Hugo Herbelin (Oct 18 2020 at 12:55):@Karl Palmskog :
Actually, I had stopped to maintain recursive-definition as well (an ancestor of the funind plugin). So, I archived it on github.
I ported maple-mode, nfix, descente-infinie, bdds, area-method, classical-realizability, containers to v8.10 (that's already a step!). Maybe area-method (a decision procedure for geometry) would find a maintainer in coq-community, maybe @Julien Narboux (Gitter import). At least Julien would know if it is worth to be maintained.
Maple mode (an interface to import Maple simplification algorithms in Coq) could probably be advertised more (though, maybe there are now alternatives, this I don't know well).
Karl Palmskog (Oct 18 2020 at 17:27):I will open the usual coq-community issue about area-method
Last updated: Sep 23 2023 at 08:01 UTC