-
Notifications
You must be signed in to change notification settings - Fork 12
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[movies] Simplify the driver #71
Conversation
I pushed the same commit as on top of #67 to test the latest |
Looks nice ! |
Yes, to merge this PR and #67, there are two options:
|
2ab0b1e
to
32fee29
Compare
Something I've just noticed is that ever since this PR, the "Build Alectryon snippets" step in the build-doc job does nothing and all the snippet building is actually done in the "Compile LaTeX document" step. I don't really understand why that would be the case given that the |
Thanks for catching that, fixed in #84 |
This is a follow-up to #70
With the change that I suggested there, I was able to refactor the movies script into a standard Alectryon pipeline, with just a few custom actions to isolate snippets in the source
.v
file.@Casteran I tried to make a minimally invasive patch, so I didn't touch the source files. Instead I just made the code look for existing
(*| .. coq:: …flags… |*)
annotations and propagate the corresponding flags.I kept the folder structure, and AFAICT the only differences are spaces; I hope I didn't miss anything (I made it so that spaces before and after snippets get stripped (which is a bit tricky due to
(*| .. coq |*)
visibility annotations).This pipeline doesn't go through reST at all.
(*| .. coq |*)
visibility annotations outside of snippets are ignores. Visibility settings get reset after each snippet, so(*||*)
can be useful in the middle of a snippet but is not needed at the end of a snippet.The syntax
(* begin snippet ABC:: …flags… *)
is supported but not used (to avoid a larger diff than necessary.@Zimmi48 I need your help to pull the latest Alectryon.