Stream: Coq users

Topic: coq-contribs


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

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 20:03):

That code is much older, since 8.10 is from 2019

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 20:03):

(https://github.com/coq/coq/releases/tag/V8.10.0)

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

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 20:06):

the authors might have used an older Coq, but hopefully not (that'd be mean)

view this post on Zulip Paolo Giarrusso (Oct 15 2020 at 20:07):

I doubt such old Coq versions support VsCoq, coqide and emacs are the likely options.

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

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

view this post on Zulip Anton Trunov (Oct 15 2020 at 20:13):

8.4 is there

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

view this post on Zulip Karl Palmskog (Oct 15 2020 at 23:03):

to get "full" VsCode support, one must copy Make to _CoqProject though

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

view this post on Zulip Karl Palmskog (Oct 16 2020 at 00:18):

where does it say that master is the latest version for contribs generally?

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 00:19):

it's the default branch. GitHub lets you change that.

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

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 00:21):

Well, so after the move there's a usability/discoverability bug.

view this post on Zulip Karl Palmskog (Oct 16 2020 at 00:22):

have you read this part about contribs generally? https://github.com/coq-community/manifesto#faq

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

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 00:24):

well, I haven't said that somebody has to fix it

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 00:25):

and I should say: thanks for suggesting a better solution!

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 00:26):

but to the "why on Earth...", it's because the correct solution was not discoverable enough.

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

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 00:27):

bug != somebody must fix it

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 00:28):

especially for usability bugs, it's tons of work

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

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

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 00:30):

I'm not sure this debate is useful, but to me GitHub does imply a spec.

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 00:31):

Focusing on "actionable things", GitHub _allows_ marking "ghost town" by archiving them, tho nobody _has_ to.

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

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

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

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

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

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

view this post on Zulip Paolo Giarrusso (Oct 16 2020 at 00:41):

And next time, if I remember, I'll check branches and tags.

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

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

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

view this post on Zulip Théo Zimmermann (Oct 16 2020 at 12:21):

(like we have successfully done many times in the past)

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

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

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

Some 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.

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

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

view this post on Zulip Karl Palmskog (Oct 16 2020 at 22:12):

same for legacy-field and rational

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

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

view this post on Zulip Hugo Herbelin (Oct 17 2020 at 09:41):

Karl Palmskog said:

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

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

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

view this post on Zulip Karl Palmskog (Oct 18 2020 at 17:27):

I will open the usual coq-community issue about area-method


Last updated: Jan 29 2023 at 01:02 UTC