Has anyone ever used Alectryon in slides for a presentation?

Not me, but you might be interested in our infrastructure / driver for inserting snippets generated with Alectryon in a LaTeX file: https://github.com/coq-community/hydra-battles/tree/master/doc/movies

It's a nice idea. wacoq/jscoq is a good alternative.

Théo Zimmermann said:

Not me, but you might be interested in our infrastructure / driver for inserting snippets generated with Alectryon in a LaTeX file: https://github.com/coq-community/hydra-battles/tree/master/doc/movies

I gave a small presentation this week (a pdf file documenting a small proof of well-foundedness)

I still have to make a small tutorial about how the snippets were generated from decorated `.v`

files.

I would be super happy to read that tutorial! But in the mean time, did you use beamer together with the infrastructure Théo was referencing, or did you use some other tool to make the slides themselves, or did you simply generate images / things that you then imported (making the tool used for the slides basically irrelevant for my question)?

I used the infrastructure Théo was talking about.

The main steps are described in https://hal.archives-ouvertes.fr/view/index/docid/3404668 (section 4.1 )

The code inclusions have been generated with Alectryon.

Indeed, since the order of code inclusions in the pdf is independent from the structure of the libraries, we import in the `.tex`

files the snippets declared in the `.v`

sources.

At the compilation of the document, Alectryon searchs for the snippets in the `.v`

, and convert them into latex blocks, which are inserted by `\input`

in the document.

- Alectryon and the hydra/latex plugin are amazing :heart:
- Is there any way of setting the maximum line length in the output? I can manually break long lines in Coq code, but not in, say, goals. I hoped
`--long-line-threshold`

might help, but nothing seems to have changed.

ping @Clément Pit-Claudel who is the person most likely to be able to answer about maximum line length

it's nice that you got the toolchain to work Ana, I think we [hydras maintainers] should probably spend time on packaging the new Python code that currently lives outside of Alectryon though. I personally find the Makefiles and scripting a bit obscure.

I assume you tried that https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:opt.Printing-Width?

No! I didn't know that was a thing! It never occurred to me that the problem might be solvable from the Coq side.

It works like a charm, thank you very much!

That's because Coq used to be a thing that you run in your terminal.

Ana de Almeida Borges said:

Has anyone ever used Alectryon in slides for a presentation?

I have, for the Alectryon talk among others :) I used reStructuredText, but @Erik Martin-Dorel recently asked whether something similar would be possible with Beamer, which led to this branch in the Alectryon repo and this example (the idea is that you use Alectryon as a `TeX → TeX`

preprocessor)

The Hydras infrastructure is another good approach, I think. What's missing in the latex frontend in the branch I linked to is a way to convert back and forth between `.tex`

and `.v`

.

Ana de Almeida Borges said:

It works like a charm, thank you very much!

Good to see that the problem was solved quickly, thanks @Théo Zimmermann :) Another way (using a custom driver) is to change `alectryon.serapi.DEFAULT_PP_ARGS['pp_margin']`

(the default is 55); there's a recipe in the repo.

Awesome! Thank you very much for the tool and for the pointers. :)

Thanks for giving Alectryon a try! If you make the results public please send me a DM, I'll add a link in the gallery at the end of the README :)

For future reference, here are the slides I ended up making. This would have been impossible without Alectryon and without the hydra snippets! Thank you :heart:

Cool! I couldn't help but notice that your example with `Set Printing Parentheses`

on the extra slide "Notations and priority" doesn't have parentheses around `All x B`

, which seems weird to me. Is that a Coq bug?

how do you measure words in Coq files? Or is it lines of code? See also "de Bruijn factor" (https://www.cs.ru.nl/~freek/factor/)

slides look very nice by the way.

also one comment if there are PL CS people there: they might want to know how/if you did capture-avoiding substitution in the logic (de Bruijn indexes, locally nameless, etc.)

Théo Zimmermann said:

Cool! I couldn't help but notice that your example with

`Set Printing Parentheses`

on the extra slide "Notations and priority" doesn't have parentheses around`All x B`

, which seems weird to me. Is that a Coq bug?

I hadn't noticed! (Didn't end up showing the slide) That is extremely odd. I guess it might indeed be a bug.

Karl Palmskog said:

how do you measure words in Coq files? Or is it lines of code? See also "de Bruijn factor" (https://www.cs.ru.nl/~freek/factor/)

In the easiest / most naive way possible, namely `g Ctrl+G`

in vim. I originally did lines of code, but I don't break down long lines in latex, so it wasn't really comparable. Thanks for the link, that is super interesting!

Karl Palmskog said:

also one comment if there are PL CS people there: they might want to know how/if you did capture-avoiding substitution in the logic (de Bruijn indexes, locally nameless, etc.)

I didn't, the names of the variables matter. Curiously enough, this wasn't really problematic for proving soundness. Perhaps it helped that I also didn't assume alpha-conversion in the paper proof, so the translation was completely straightforward in that regard. But now that I'm proving completeness, I'm having a lot of work that perhaps would have been avoided by a different implementation.

I opened a report for the parentheses non-printing: https://github.com/coq/coq/issues/15322

but if I may ask, how does https://gitlab.com/ana-borges/QRC1-Coq/-/blob/ProofSociety/theories/Language.v#L257-267 implements capture-avoiding substitution? In `| All y B => if Var y == t1 then All y B else All y B``[t1 <- t2]`

, it seems `y`

can occur free in `t2`

…

It can! But in every lemma where this matters there is an assumption that all substitutions are safe.

Oh. Interesting twist.

but without alpha-renaming, how do you instantiate `\forall x, P(x)`

with `x`

to get `P(x)`

? Must one choose distinct variables in advance?

In practical use cases when you have very specific formulas and want to compute stuff, I suppose you would need to pick suitable names, yes. I admit this is not a situation I have ran into. When proving things about abstract formulas it is easy to assume stuff.

if you can quantify over propositions (which isn’t possible in first-order logic), that might not even be an option, since a proposition can be duplicated, so “all distinct variables” isn’t necessarily preserved... Here it might be possible to just never reuse variables.

But instantiating `\forall x, P x`

with `x`

to get `P x`

seems trivial, so perhaps I'm not understanding your question

in lambda calculus, “keep all variables distinct” during reduction definitely needs alpha-renaming during reduction — I know because I once realized I got this wrong, close to a deadline

@Ana de Almeida Borges hm, I guess I should have said “instantiate `\forall y x, P(y)`

with `x`

— without capture-avoidance (or a side-condition), that produces `\forall x, P(x)`

instead of `\forall z, P(x)`

.

with sufficient side-condition, the proof would just not be possible, so you need to go back and pick more distinct variables.

anyway, I’m not sure how bad this is for a first-order logic; sorry for the OT, I mostly nerd-sniped myself.

Ah, in that case there is no way of easily doing it right now. It's easy to prove alpha-conversion in the calculus, but other than that, this situation would not lead anywhere without backtracking and picking more suitable names.

Well, I've heard the prophecies that one should always use de Brujin indexes and have been waiting for the sword to fall over my head since more or less the beginning. Just not enough to actually learn how to implement them. (I should mention that I didn't seriously think I would stick with this project at first.)

Part of it is curiosity over what exactly happens when you ignore the warnings and use relevant names. For now, the answer seems to be "not much", although I think I might be a victim of sticking with an idea even when doing so might not be very efficient. Also, I don't have a good model of what would become easier with irrelevant names, so this experience is a bit underpowered for now.

I was told exactly that was the story behind http://r6.ca/Goedel/goedel1.html.

There substitution is capture-avoiding, but not structural.

I've also seen "mechanized" paper submissions where some theorems were not actually mechanized in full generality.

In any case, conventional de Bruijn indexes are also somewhat ugly. I find https://www.ps.uni-saarland.de/Publications/documents/SchaeferEtAl_2015_Autosubst_-Reasoning.pdf and successors more elegant — and they also have a decision procedure for binding lemmas! (Sadly, a slow one).

Paolo Giarrusso said:

There substitution is capture-avoiding, but not structural.

This looks supremely painful

Paolo Giarrusso said:

I've also seen "mechanized" paper submissions where some theorems were not actually mechanized in full generality.

Well. At first glance this sounds awful, but upon further thinking it just seems reasonable. I'm guilty of it (well, there is no submitted paper) in that I am only using finite sets in Coq, for example.

Paolo Giarrusso said:

In any case, conventional de Bruijn indexes are also somewhat ugly. I find https://www.ps.uni-saarland.de/Publications/documents/SchaeferEtAl_2015_Autosubst_-Reasoning.pdf and successors more elegant — and they also have a decision procedure for binding lemmas! (Sadly, a slow one).

Ooh, I should take a closer look at this, thanks!

Finite sets seem reasonable; but they had a theorem for all terms, that they could only mechanize on closed terms. They fixed it in time, but I suspect it was very painful.

Depending on your use case, Autosubst 2 might be better to use than Autosubst 1. We are using it in the Coq Library of Undecidability to formalise first-order logic, second-order logic, STLC, and System F

Sorry, I agree Autosubst 2 is often what one should use (even if I never did), but the Autosubst 1 paper is IMHO still where you want to start learning.

But "and successors" was too obscure, so thanks for the correction Yannick :grinning:

Last updated: Jun 16 2024 at 01:42 UTC