Pierre Castéran

Indeed, I think I will spend at least a few weeks (months ?) to - adapt to Alectryon the files part-hydras.tex and chapter-primrec.tex - develop .v files in theories/gaia (and...

Perhaps we should also provide a tar file of the html files, with instructions for making the links `../theories/html` correct ? > Le 26 août 2021 à 22:44, Karl Palmskog...

Thanks for your comments ! I will follow your advice about vertical spacing. I will come back to you when I have some corrected examples. > This actually leads me...

Removing the blank lines around the beginning and end of snippets helps a lot! > Le 27 août 2021 à 10:27, Clément Pit-Claudel ***@***.***> a écrit : > > >...

I noted a small issue: I wanted to implement the pattern "rest of proof skipped", for instance through the snippet mGeb (in file theories/ordinals/Hydra/Omega_Small.v) I couldn't unstick the final `Qed`from...

I like the idea of including multiple snippets ! Besides the issue of spacing, I believe it will make the latex source more readable. > Le 29 août 2021 à...

@Zimmi48 The last version I pushed fails almost immediately on NIX CI on the "Checking presence of CI target coq" step. Is this just a problem of the machine which...

> > Perhaps we should also provide a tar file of the html files, with instructions for making the links `../theories/html` correct ? > > Indeed, we can provide a...

Coqdoc generation fails on NIX CI with a message I don't understand. (works on my machine) File "./theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v", line 6, characters 0-78: Error: /home/runner/work/hydra-battles/hydra-battles/theories/ordinals/OrdinalNotations/ON_Finite.vo: premature end of file. Try to...

It works now! All the chapters of the book use Alectryon. There are still a few verbatim (source and answers) when the computations are too long or result in errors...