Ana de Almeida Borges (Nov 16 2021 at 18:11): Ana de Almeida Borges (Nov 16 2021 at 18:11):Has anyone ever used Alectryon in slides for a presentation?
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
Bas Spitters (Nov 17 2021 at 10:27):It's a nice idea. wacoq/jscoq is a good alternative.
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.
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)?
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.
Ana de Almeida Borges (Nov 23 2021 at 19:08):--long-line-threshold might help, but nothing seems to have changed. 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
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.
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?
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.
Ana de Almeida Borges (Nov 23 2021 at 19:36):It works like a charm, thank you very much!
Théo Zimmermann (Nov 23 2021 at 19:47):That's because Coq used to be a thing that you run in your terminal.
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)
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.
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.
Ana de Almeida Borges (Nov 23 2021 at 23:58):Awesome! Thank you very much for the tool and for the pointers. :)
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 :)
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:
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?
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/)
Karl Palmskog (Dec 09 2021 at 18:07):slides look very nice by the way.
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.)
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 Parentheseson the extra slide "Notations and priority" doesn't have parentheses aroundAll 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.
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!
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.
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
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…
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.
Paolo Giarrusso (Dec 10 2021 at 00:35):Oh. Interesting twist.
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?
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.
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.
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
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
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).
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.
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.
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.
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.)
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.
Paolo Giarrusso (Dec 10 2021 at 00:53):I was told exactly that was the story behind http://r6.ca/Goedel/goedel1.html.
Paolo Giarrusso (Dec 10 2021 at 00:56):There substitution is capture-avoiding, but not structural.
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.
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).
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
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.
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!
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.
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
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.
Paolo Giarrusso (Dec 10 2021 at 13:10):But "and successors" was too obscure, so thanks for the correction Yannick :grinning:
Last updated: Apr 19 2024 at 00:02 UTC