Old Coq modules · Miscellaneous · Zulip Chat Archive

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

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.

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.

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.

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)

Karl Palmskog (Aug 16 2022 at 20:59):

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

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.

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.

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.

Pierre-Marie Pédrot (Aug 17 2022 at 11:36):

Better than testing it, prove it correct...

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

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?

Pierre-Marie Pédrot (Aug 17 2022 at 21:52):

I think that matter was never settled.

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.

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

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?

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.

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)

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.

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?

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.

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