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...
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.
There is a semi-privately circulating archive with implementations from the darkest ages of Coq, i.e. starting from 1984.
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.
(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)
aren't there some CoC examples also in https://github.com/coq-contribs/coq-in-coq
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.
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.
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.
Better than testing it, prove it correct...
@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
@Pierre-Marie Pédrot do old Coq version not belong to INRIA or other French public institutions?
I think that matter was never settled.
IANAL, but AFAIK in France software produced by researchers does not belong to their employers.
Summoning @Maxime Dénès because I think he tried to look into that issue by asking lawyer-y people at INRIA, IIRC
@Pierre-Marie Pédrot do old Coq version not belong to INRIA or other French public institutions?
Why would they? They were written by INRIA researchers, and if what I wrote above is true, it should be legally theirs.
(well, not only INRIA, and I think this is part of the problem, because this ownership doesn't apply to other positions)
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.
@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?
We have many versions there, so probably not. But we can have different licenses for every release or so.
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).
There are so many illegal public archives of abandonware...
doesn't this code even belong with some software history preservation archive?
for example: https://computerhistory.org/software-history-center/
Probably, but [insert here some ranting about the absurd copyright system we live in]
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.
sure, so maybe the most interesting parts are the actual Coq .v(?) code examples
Sweet summer child! The old Coq files are actually strings written directly in ML, following the glorious HOL minimalist approach.
here is Newman's lemma from Coq 1.10: https://gist.github.com/ppedrot/50159f6dbfeacd067ae07327f9887c37
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
(I don't know why these people were obsessed with Newman's lemma, it's all over the place)
I think it's usually used when teaching people rewriting systems?
which I think Huet was doing at least some of the time
Last updated: May 31 2023 at 04:01 UTC