Moving to Alectryon : first draft

[Casteran]

@start974 @Zimmi48 @palmskog @cpitclaudel

The part of hydra-battles's documentation dedicated to ordinals is now made with Alectryon. (sniipets extracted from theories/ordinals//.v )

This document is stiil a draft, and I will re-read it slowly now. After the corrections, it would be nice to make a release.

I noticed two issues:

• sometimes, the implication arrow -> is broken into two pieces (in long formulas) .
• There were also big vertical spaces between two adjacent snippets.

Many thanks to all of you !

[palmskog]

@Casteran some high-level comments on what I think would be beneficial for a release:

• Consider switching from italicized text inside "Project" and "Exercise" blocks to plain text. Tilted fixed-width syntax looks bad and is hard to read, even using Alectryon. Project 2.2 on page 23 is one example.
• Consider putting the release pdf on GitHub as an asset. One example is the Coq 8.13.2 release, which includes the reference manual as pdf, and another is the Mathematical Components book 1.0.0 release.
• Consider putting the source code and pdf on Zenodo to enable citing both the text and code. One example is the Coq 8.13.0 release, and another is the MCB 1.0.0 release.

[cpitclaudel]

Awesome work :)

The spacing issue is due to the way the chopping into snippets is done; it produces this:

\begin{alectryon}
  \begin{txt}
    \nl
  \end{txt}
  \sep
  \begin{sentence}
    \begin{input}
      \PY{k+kn}{Inductive}~\PY{n+nf}{S0}~\PY{o}{:}~~\PY{n}{relation}~\PY{n}{Hydrae}~\PY{o}{:=}\nl
        …
    \end{input}
  \end{sentence}
  \sep
  \begin{txt}
    \nl
  \end{txt}
\end{alectryon}

The \begin{txt} \nl \end{txt} at the beginning and end of each snippet are blank lines, hence the trouble. This is because the original snippet has newlines in it too.

(* begin snippet S0Def *)

Inductive S0 :  relation Hydrae :=
| S0_first : forall s, S0  (hcons head s) s
| S0_rest : forall  h s s',
    S0  s s' ->  S0  (hcons h s) (hcons h s').

(* end snippet S0Def *)

This can be fixed in extract_snippets/Extractor.py, I'm sure. I can look into it if needed. But I think it would be simpler to fix it with a transform (before generating the LaTeX code).

This actually leads me to another point that I wanted to discuss. Right now the converter does coq → reStructuredText → LaTeX → LaTeX snippets. But the only reStructuredText feature that is used is setting display flags using .. coq:: …, I think. (Is that right?)

If that's the case, there would be a simpler and faster design, which would also pollute the source code less. Instead of

  (* begin snippet endOfProof *)

  (*| .. coq:: no-out |*)

  …

we would write

  (* begin snippet endOfProof:: no-out *)

  …

There would be no need for reStructuredText. Additionally, the segmentation would be a lot simpler: we would do coq → list of coq fragments → LaTeX snippets. That is, we would cut up the document into snippets, and then feed it to Coq, instead of the other way around.

And this would address the issues that Pierre noted with the amount of LaTeX that gets generated, and hence the need to add no-out in many places outside of snippets to reduce the size of the generated document. Instead we would simply not convert to latex things that are not part of snippets.

There's just one thing that's convenient with reStructuredText's directives that wouldn't be as easy: changing flags mid-way through a snippet. That is, there's no immediate equivalent of this:

  (* begin snippet endOfProof *)

  (*| .. coq:: no-out |*)

  …

  (*| .. coq:: messages |*)

  …

Pierre, is this a pattern that you use a lot? If so we can think of tweaks/fixes. It shouldn't be too hard to add.

[Casteran]

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 @.***> a écrit :

@Casteran https://github.com/Casteran some high-level comments on what I think would be beneficial for a release:

Consider switching from italicized text inside "Project" and "Exercise" blocks to plain text. Tilted fixed-width syntax looks bad and is hard to read, even using Alectryon. Project 2.2 on page 23 is one example. Consider putting the release pdf on GitHub as an asset. One example is the Coq 8.13.2 release https://github.com/coq/coq/releases/tag/V8.13.2, which includes the reference manual as pdf, and another is the Mathematical Components book 1.0.0 release https://github.com/math-comp/mcb/releases/tag/zenodo-1.0.0. Consider putting the source code and pdf on Zenodo to enable citing both the text and code. One example is the Coq 8.13.0 release https://zenodo.org/record/4501022, and another is the MCB 1.0.0 release https://zenodo.org/record/4282710. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq-community/hydra-battles/issues/70#issuecomment-906730067, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCRJMMJ34N6PK2BVDBTT62RSJANCNFSM5C36J2AA. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

[palmskog]

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 separate archive with HTML files. But in this case, I suggest manually preprocessing the HTML files to fix any linking issues before attaching this archive. Even better would in my opinion be that the main source archive contains the manually preprocessed HTML files (correct links) along with Coq source files.

[Casteran]

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 to another point that I wanted to discuss. Right now the converter does coq → reStructuredText → LaTeX → LaTeX snippets. But the only reStructuredText feature that is used is setting display flags using .. coq:: …, I think. (Is that right?)

Yes, for the time being ...

If that's the case, there would be a simpler and faster design, which would also pollute the source code less. Instead of

( begin snippet endOfProof )

(| .. coq:: no-out |)

… we would write

( begin snippet endOfProof:: no-out )

Ok, I will try. … There would be no need for reStructuredText. Additionally, the segmentation would be a lot simpler: we would do coq → list of coq fragments → LaTeX snippets. That is, we would cut up the document into snippets, and then feed it to Coq, instead of the other way around.

And this would address the issues that Pierre noted with the amount of LaTeX that gets generated, and hence the need to add no-out in many places outside of snippets to reduce the size of the generated document. Instead we would simply not convert to latex things that are not part of snippets.

There's just one thing that's convenient with reStructuredText's directives that wouldn't be as easy: changing flags mid-way through a snippet. That is, there's no immediate equivalent of this:

( begin snippet endOfProof )

(| .. coq:: no-out |)

…

(| .. coq:: messages |)

… Pierre, is this a pattern that you use a lot? If so we can think of tweaks/fixes. It shouldn't be too hard to add.

Indeed, in long proofs, I may start with the no-out for important proof steps, like transfinite induction, assert, etc., then display a bunch of sub-goals, then usenoneto mask boring or shameful details … Perhaps a good solution would be to cut a snippet into homogeneous slices, at the cost of adding a lot of comments to the.vfile. I didn’t tryalectryon.el` yet. Could it be used to mask all the Alectryon directives ?

Anyway, thank you for this tool !!! Pierre

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq-community/hydra-battles/issues/70#issuecomment-907025321, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCWOVZKBB7ZCEHYLYGTT65D7HANCNFSM5C36J2AA. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

[Casteran]

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 :

Awesome work :)

The spacing issue is due to the way the chopping into snippets is done; it produces this:

\begin{alectryon} \begin{txt} \nl \end{txt} \sep \begin{sentence} \begin{input} \PY{k+kn}{Inductive}~\PY{n+nf}{S0}~\PY{o}{:}~~\PY{n}{relation}~\PY{n}{Hydrae}~\PY{o}{:=}\nl … \end{input} \end{sentence} \sep \begin{txt} \nl \end{txt} \end{alectryon} The \begin{txt} \nl \end{txt} at the beginning and end of each snippet are blank lines, hence the trouble. This is because the original snippet has newlines in it too.

( begin snippet S0Def )

Inductive S0 : relation Hydrae := | S0_first : forall s, S0 (hcons head s) s | S0_rest : forall h s s', S0 s s' -> S0 (hcons h s) (hcons h s').

( end snippet S0Def ) This can be fixed in extract_snippets/Extractor.py, I'm sure. I can look into it if needed. But I think it would be simpler to fix it with a transform (before generating the LaTeX code).

This actually leads me to another point that I wanted to discuss. Right now the converter does coq → reStructuredText → LaTeX → LaTeX snippets. But the only reStructuredText feature that is used is setting display flags using .. coq:: …, I think. (Is that right?)

If that's the case, there would be a simpler and faster design, which would also pollute the source code less. Instead of

( begin snippet endOfProof )

(| .. coq:: no-out |)

… we would write

( begin snippet endOfProof:: no-out )

… There would be no need for reStructuredText. Additionally, the segmentation would be a lot simpler: we would do coq → list of coq fragments → LaTeX snippets. That is, we would cut up the document into snippets, and then feed it to Coq, instead of the other way around.

And this would address the issues that Pierre noted with the amount of LaTeX that gets generated, and hence the need to add no-out in many places outside of snippets to reduce the size of the generated document. Instead we would simply not convert to latex things that are not part of snippets.

There's just one thing that's convenient with reStructuredText's directives that wouldn't be as easy: changing flags mid-way through a snippet. That is, there's no immediate equivalent of this:

( begin snippet endOfProof )

(| .. coq:: no-out |)

…

(| .. coq:: messages |)

… Pierre, is this a pattern that you use a lot? If so we can think of tweaks/fixes. It shouldn't be too hard to add.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq-community/hydra-battles/issues/70#issuecomment-907025321, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCWOVZKBB7ZCEHYLYGTT65D7HANCNFSM5C36J2AA. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

[Zimmi48]

… we would write ( begin snippet endOfProof:: no-out ) Ok, I will try.

Note that this is just an idea but this is not supported yet.

[cpitclaudel]

I looked a bit further, and it does sound like we would need some syntax for changing the default rendering past for part of a snippet, since there are many uses of that feature.

I will think about it.

[cpitclaudel]

OK, implementation is in #71.

I will think about it.

I went the easiest way possible: I implemented (* begin snippet endOfProof:: no-out *) headers, and I further subdivide snippets around comments of the form (*| .. coq:: … |*), keeping track of the relevant output customizations for each sub-snippet; they are all reassembled in the end..

[Casteran]

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 Qedfrom the comment (* ... *) in the pdf (p. 45). I tried a workaround: to add a snippet just for the final Qed. More generally, A possible way to show only parts of a proof script would be to use a sequence of snippets instead of a single one with sub-snippets in nonemode ?

The issue is visible on the last commited version.

[cpitclaudel]

Thanks, that's a mistake I made in the coalesce_text function in Alectryon (I wrote it a while ago but didn't use it until this project). And indeed after the fix:

diff --git a/snippets.broken-concat/Omega2_Small/mGeb.tex b/snippets/Omega2_Small/mGeb.tex
index 0e829ab..00e1e78 100644
--- a/snippets.broken-concat/Omega2_Small/mGeb.tex
+++ b/snippets/Omega2_Small/mGeb.tex
@@ -2,12 +2,13 @@
   % Generator: Alectryon
   \sep
   \begin{txt}
-    ~~~~\PY{c}{(*~...~*)}
+    ~~~~\PY{c}{(*~...~*)}\nl
+    ~~~~~~\nl
   \end{txt}
   \sep
   \begin{sentence}
     \begin{input}
-      \PY{k+kn}{Qed}\PY{o}{.}
+      ~~\PY{k+kn}{Qed}\PY{o}{.}
     \end{input}
   \end{sentence}
 \end{alectryon}

[cpitclaudel]

More generally, A possible way to show only parts of a proof script would be to use a sequence of snippets instead of a single one with sub-snippets in nonemode ?

Yes, but there will be problems with spacing, since you'll have two snippets and hence two alectryon environments.

I do think it would be cleaner to have multiple snippets with no .. coq:: none comments in the middle of them, tough (it would further simplify the driver, too). If you want to go that route, then we would change the LaTeX slightly: you would have a command \includesnippets{snippet1,snippet2,snippet3} instead of a plain \include, and that command would include all three snippets in a single \alectryon block.

Let me know if you want to do that.

[Casteran]

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 à 19:41, Clément Pit-Claudel @.***> a écrit :

More generally, A possible way to show only parts of a proof script would be to use a sequence of snippets instead of a single one with sub-snippets in nonemode ?

Yes, but there will be problems with spacing, since you'll have two snippets and hence two alectryon environments.

I do think it would be cleaner to have multiple snippets with no .. coq:: none comments in the middle of them, tough (it would further simplify the driver, too). If you want to go that route, then we would change the LaTeX slightly: you would have a command \includesnippets{snippet1,snippet2,snippet3} instead of a plain \include, and that command would include all three snippets in a single \alectryon block.

Let me know if you want to go that route.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/coq-community/hydra-battles/issues/70#issuecomment-907835842, or unsubscribe https://github.com/notifications/unsubscribe-auth/AJW6FCSWMTJKL6TGCHTKATDT7JWLPANCNFSM5C36J2AA. Triage notifications on the go with GitHub Mobile for iOS https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Android https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.

[cpitclaudel]

sometimes, the implication arrow -> is broken into two pieces (in long formulas) .

Fixed in #72

[cpitclaudel]

I like the idea of including multiple snippets !

OK, prototype in #73

[Casteran]

@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 runs CI ? Or a mistake of mine ?

[Zimmi48]

The error is surprising, especially because it doesn't give any useful output to debug it. It's likely though that this will be a transient error so let's wait to see if it persists.

[Casteran]

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 separate archive with HTML files. But in this case, I suggest manually preprocessing the HTML files to fix any linking issues before attaching this archive. Even better would in my opinion be that the main source archive contains the manually preprocessed HTML files (correct links) along with Coq source files.

So, What you suggest is to generate (by coqdoc -g -html Foo.v) a file Foo.htmlwhich will be in the same directory as Foo.v?

[palmskog]

So, What you suggest is to generate (by coqdoc -g -html Foo.v) a file Foo.htmlwhich will be in the same directory as Foo.v?

Recall that a GitHub tag/release generates a tarball with the contents of the repo (possibly excepting some files). This means the user has to run make html manually to get the HTML files in theories/html. I was suggesting to prepare a release archive/tarball manually (in addition to the generated one) to have these HTML files already included in the usual directory (theories/html).

[Casteran]

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

"coqc" -q -w -notation-overridden -w -ambiguous-paths -w -deprecated-instance-without-locality -w -deprecated-hint-rewrite-without-locality -R theories/ordinals hydras -R theories/additions additions -R theories/gaia gaia_hydras -R exercises hydra_exercises theories/ordinals/OrdinalNotations/ON_plus.v make[1]: [Makefile.coq:724: theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.glob] Error 1 make[1]: Waiting for unfinished jobs.... make[1]: Leaving directory '/home/runner/work/hydra-battles/hydra-battles' make: *** [Makefile:5: html] Error 2 Error: Process completed with exit code 2.

[Casteran]

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 during the snippet extraction. I have now to look for typos, overfull boxes, ... ¡ Mañana !

[cpitclaudel]

!! :tada: :partying_face: