Stream: Miscellaneous

Topic: Old Coq modules


view this post on Zulip Pedro Minicz (Aug 16 2022 at 18:29):

In the comments of Andrej Bauer's blog post How to implement dependent type theory III someone named Flavio mentions old Coq modules from before inductive types were added. I looked for these old modules, but I couldn't find them. Anyone knows where I can find them?

Flavio's original comment:

When i implemented a dependent type checker the best test i found was to take old Coq modules (old versions that didn't have inductive types) and run then thru the checker... Really awesome feeling when you get it to work out some complicated examples...

view this post on Zulip Karl Palmskog (Aug 16 2022 at 20:36):

the oldest Coq releases that are archived are from 1991, version 5.6: https://coq.inria.fr/distrib/

Inductive types were already added back then. The versions of Coq without inductive types were probably from the 80s, so not clear the code is still available.

view this post on Zulip Pierre-Marie Pédrot (Aug 16 2022 at 20:51):

There is a semi-privately circulating archive with implementations from the darkest ages of Coq, i.e. starting from 1984.

view this post on Zulip Pierre-Marie Pédrot (Aug 16 2022 at 20:51):

We basically never agreed on a license for it so the legal status is unclear, but I've been advocating for its official publication somewhere for a bit of time already.

view this post on Zulip Pierre-Marie Pédrot (Aug 16 2022 at 20:54):

(not sure it's really helpful as a test suite for CoC because there are few examples in the repo, and the syntax is antiquated)

view this post on Zulip Karl Palmskog (Aug 16 2022 at 20:59):

aren't there some CoC examples also in https://github.com/coq-contribs/coq-in-coq

view this post on Zulip Pedro Minicz (Aug 17 2022 at 11:28):

Pierre-Marie Pédrot said:

We basically never agreed on a license for it so the legal status is unclear, but I've been advocating for its official publication somewhere for a bit of time already.

That is unfortunate. I'd hope these files would be under an unencumbered open-source license.

view this post on Zulip Pedro Minicz (Aug 17 2022 at 11:28):

Karl Palmskog said:

aren't there some CoC examples also in https://github.com/coq-contribs/coq-in-coq

Oh, thanks for the link. I'll see if I can find what I want in that repo.

view this post on Zulip Pedro Minicz (Aug 17 2022 at 11:31):

It is not so easy to find term to test a CC implementation as I would expect. I found papers describing how to exhaustively generate small STLC terms and randomly generate large STLC terms, but so far no much success in finding a way to extensively test the dependent part of my toy type-checker.

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2022 at 11:36):

Better than testing it, prove it correct...

view this post on Zulip Paolo Giarrusso (Aug 17 2022 at 19:23):

@Pedro Minicz FWIW, if you want a toy CoC implementation, you might be able to use existing PTS interpreters; google should find the one by Toxaris and the one by dolio

view this post on Zulip Paolo Giarrusso (Aug 17 2022 at 19:24):

@Pierre-Marie Pédrot do old Coq version not belong to INRIA or other French public institutions?

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2022 at 21:52):

I think that matter was never settled.

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2022 at 21:53):

IANAL, but AFAIK in France software produced by researchers does not belong to their employers.

view this post on Zulip Pierre-Marie Pédrot (Aug 17 2022 at 21:54):

Summoning @Maxime Dénès because I think he tried to look into that issue by asking lawyer-y people at INRIA, IIRC

view this post on Zulip Paolo Giarrusso (Aug 18 2022 at 11:31):

@Pierre-Marie Pédrot do old Coq version not belong to INRIA or other French public institutions?

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2022 at 11:32):

Why would they? They were written by INRIA researchers, and if what I wrote above is true, it should be legally theirs.

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2022 at 11:33):

(well, not only INRIA, and I think this is part of the problem, because this ownership doesn't apply to other positions)

view this post on Zulip Maxime Dénès (Aug 18 2022 at 11:55):

Hi! I don't remember looking into that particular issue. What we tried to do was to collect all the institutions having hired Coq contributors, in case we needed for example their agreement for a license change. AFAIK, this process more or less failed (at least we can't be sure to have identified all organizations). This would probably be make the publication of the old archive more difficult, although maybe not impossible.

view this post on Zulip Maxime Dénès (Aug 18 2022 at 11:56):

@Pierre-Marie Pédrot Are you sure contributors were all working for Inria at the time they worked on versions up to the one that is in this archive?

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2022 at 12:00):

We have many versions there, so probably not. But we can have different licenses for every release or so.

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2022 at 12:02):

That said we're really too picky here. I've already put this archive on the internet, although you have to know where to get it (hint: not very hard). And I'm willing to sustain any legal turmoil that would follow (that is, probably none).

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2022 at 12:04):

There are so many illegal public archives of abandonware...

view this post on Zulip Karl Palmskog (Aug 18 2022 at 12:05):

doesn't this code even belong with some software history preservation archive?

view this post on Zulip Karl Palmskog (Aug 18 2022 at 12:05):

for example: https://computerhistory.org/software-history-center/

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2022 at 12:05):

Probably, but [insert here some ranting about the absurd copyright system we live in]

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2022 at 12:07):

Most of the code from the Coq archive is not compilable today. It used old versions of Caml Lourd, LeLISP or other long forgotten research compilers.

view this post on Zulip Karl Palmskog (Aug 18 2022 at 12:09):

sure, so maybe the most interesting parts are the actual Coq .v(?) code examples

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2022 at 12:10):

Sweet summer child! The old Coq files are actually strings written directly in ML, following the glorious HOL minimalist approach.

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2022 at 12:12):

here is Newman's lemma from Coq 1.10: https://gist.github.com/ppedrot/50159f6dbfeacd067ae07327f9887c37

view this post on Zulip Karl Palmskog (Aug 18 2022 at 12:12):

ah right, but even HOL has stuff like this these days:

Theorem my_thm:
 T
Proof
rw []
End

even if it expands out via macros to a bunch of ML

view this post on Zulip Pierre-Marie Pédrot (Aug 18 2022 at 12:13):

(I don't know why these people were obsessed with Newman's lemma, it's all over the place)

view this post on Zulip Karl Palmskog (Aug 18 2022 at 12:14):

I think it's usually used when teaching people rewriting systems?

view this post on Zulip Karl Palmskog (Aug 18 2022 at 12:15):

which I think Huet was doing at least some of the time


Last updated: Jan 29 2023 at 19:02 UTC