Stream: Coq users

Topic: Alectryon in slides


view this post on Zulip Ana de Almeida Borges (Nov 16 2021 at 18:11):

Has anyone ever used Alectryon in slides for a presentation?

view this post on Zulip Théo Zimmermann (Nov 17 2021 at 09:20):

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

view this post on Zulip Bas Spitters (Nov 17 2021 at 10:27):

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

view this post on Zulip Pierre Castéran (Nov 17 2021 at 17:10):

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.

view this post on Zulip Ana de Almeida Borges (Nov 17 2021 at 19:12):

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

view this post on Zulip Pierre Castéran (Nov 17 2021 at 20:37):

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

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.

view this post on Zulip Ana de Almeida Borges (Nov 23 2021 at 19:08):

  1. Alectryon and the hydra/latex plugin are amazing :heart:
  2. 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.

view this post on Zulip Karl Palmskog (Nov 23 2021 at 19:10):

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

view this post on Zulip Karl Palmskog (Nov 23 2021 at 19:11):

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.

view this post on Zulip Théo Zimmermann (Nov 23 2021 at 19:30):

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

view this post on Zulip Ana de Almeida Borges (Nov 23 2021 at 19:32):

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

view this post on Zulip Ana de Almeida Borges (Nov 23 2021 at 19:36):

It works like a charm, thank you very much!

view this post on Zulip Théo Zimmermann (Nov 23 2021 at 19:47):

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

view this post on Zulip Clément Pit-Claudel (Nov 23 2021 at 22:00):

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)

view this post on Zulip Clément Pit-Claudel (Nov 23 2021 at 22:01):

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.

view this post on Zulip Clément Pit-Claudel (Nov 23 2021 at 22:04):

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.

view this post on Zulip Ana de Almeida Borges (Nov 23 2021 at 23:58):

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

view this post on Zulip Clément Pit-Claudel (Nov 24 2021 at 04:42):

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

view this post on Zulip Ana de Almeida Borges (Dec 09 2021 at 16:45):

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:

view this post on Zulip Théo Zimmermann (Dec 09 2021 at 18:03):

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?

view this post on Zulip Karl Palmskog (Dec 09 2021 at 18:06):

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

view this post on Zulip Karl Palmskog (Dec 09 2021 at 18:07):

slides look very nice by the way.

view this post on Zulip Karl Palmskog (Dec 09 2021 at 19:06):

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

view this post on Zulip Ana de Almeida Borges (Dec 09 2021 at 23:55):

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.

view this post on Zulip Ana de Almeida Borges (Dec 09 2021 at 23:58):

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!

view this post on Zulip Ana de Almeida Borges (Dec 10 2021 at 00:05):

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.

view this post on Zulip Ana de Almeida Borges (Dec 10 2021 at 00:32):

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

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 00:33):

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

view this post on Zulip Ana de Almeida Borges (Dec 10 2021 at 00:33):

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

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 00:35):

Oh. Interesting twist.

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 00:36):

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?

view this post on Zulip Ana de Almeida Borges (Dec 10 2021 at 00:38):

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.

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 00:39):

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.

view this post on Zulip Ana de Almeida Borges (Dec 10 2021 at 00:40):

But instantiating \forall x, P x with x to get P x seems trivial, so perhaps I'm not understanding your question

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 00:41):

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

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 00:42):

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

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 00:45):

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

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 00:46):

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

view this post on Zulip Ana de Almeida Borges (Dec 10 2021 at 00:47):

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.

view this post on Zulip Ana de Almeida Borges (Dec 10 2021 at 00:48):

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

view this post on Zulip Ana de Almeida Borges (Dec 10 2021 at 00:51):

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.

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 00:53):

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

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 00:56):

There substitution is capture-avoiding, but not structural.

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 00:56):

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

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 00:58):

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

view this post on Zulip Ana de Almeida Borges (Dec 10 2021 at 00:59):

Paolo Giarrusso said:

There substitution is capture-avoiding, but not structural.

This looks supremely painful

view this post on Zulip Ana de Almeida Borges (Dec 10 2021 at 01:00):

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.

view this post on Zulip Ana de Almeida Borges (Dec 10 2021 at 01:01):

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!

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 01:07):

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.

view this post on Zulip Yannick Forster (Dec 10 2021 at 12:21):

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

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 13:10):

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.

view this post on Zulip Paolo Giarrusso (Dec 10 2021 at 13:10):

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


Last updated: Jan 29 2023 at 05:03 UTC