plfa / plfa.github.io

An introduction to programming language theory in Agda
https://plfa.github.io
Creative Commons Attribution 4.0 International
1.35k stars 304 forks source link

Slow workflow for contributors #1018

Open nrnrnr opened 1 month ago

nrnrnr commented 1 month ago

As a contributor, if I want to refine text that I am editing, the only instruction I have from _site/Contributing/index.html is make build. But make build takes over 3 minutes even on a relatively beefy machine. When editing a document and viewing the changes, 3 minutes is not an acceptable turnaround time.

There must be a Makefile target somewhere that simply rebuilds the HTML of any file that has changed. That target should be documented in _site/Contributing/index.html. (If I knew the target I would submit a PR.)

It would be even better if HTML could be rebuilt without minifying.

wenkokke commented 1 month ago

That is what make build should do, so I'm unsure what's going wrong.

wenkokke commented 1 month ago

For reference, the build logic is defined in tools/Buildfile.hs.

There's probably some bug that snuck into the dependencies. Maybe due to the epub? That needs to be rebuilt after every change, and it's a bit hefty.

wenkokke commented 1 month ago

@nrnrnr Could you try running

MODE=dev cabal v2-run builder -- build
nrnrnr commented 1 month ago

I hope this is of some use. If you want, I can annotate a version that will timestamp each line of output.


nr@homedog ~/n/plfa [1]> /usr/bin/time env MODE=dev cabal v2-run builder -- build
Using Agda standard library version v1.7.2
# agda (for OracleQ (AgdaVersionQuery ()))
Using Agda version 2.6.3-c4a7cfa-dirty
# agda (for _cache/raw_agda_html/Eval/courses/TSPL/2023/Eval.md)
# agda (for _cache/raw_agda_html/Assignment4/courses/TSPL/2023/Assignment4.md)
# agda (for _cache/raw_agda_html/Assignment3/courses/TSPL/2023/Assignment3.md)
# agda (for _cache/raw_agda_html/Assignment2/courses/TSPL/2023/Assignment2.md)
# agda (for _cache/raw_agda_html/Assignment1/courses/TSPL/2023/Assignment1.md)
# agda (for _cache/raw_agda_html/Exam/courses/TSPL/2023/Exam.md)
# agda (for _cache/raw_agda_html/Eval/courses/TSPL/2022/Eval.md)
# agda (for _cache/raw_agda_html/Assignment4/courses/TSPL/2022/Assignment4.md)
# agda (for _cache/raw_agda_html/Assignment3/courses/TSPL/2022/Assignment3.md)
# agda (for _cache/raw_agda_html/Assignment2/courses/TSPL/2022/Assignment2.md)
# agda (for _cache/raw_agda_html/Assignment1/courses/TSPL/2022/Assignment1.md)
# agda (for _cache/raw_agda_html/Exam/courses/TSPL/2019/Exam.md)
# agda (for _cache/raw_agda_html/Assignment4/courses/TSPL/2019/Assignment4.md)
# agda (for _cache/raw_agda_html/Assignment3/courses/TSPL/2019/Assignment3.md)
# agda (for _cache/raw_agda_html/Assignment2/courses/TSPL/2019/Assignment2.md)
# agda (for _cache/raw_agda_html/Assignment1/courses/TSPL/2019/Assignment1.md)
# agda (for _cache/raw_agda_html/plfa.part2.Substitution/src/plfa.part2.Substitution.md)
# agda (for _cache/raw_agda_html/plfa.part3.Soundness/src/plfa.part3.Soundness.md)
# agda (for _cache/raw_agda_html/plfa.part1.Relations/src/plfa.part1.Relations.md)
# agda (for _cache/raw_agda_html/plfa.part1.Quantifiers/src/plfa.part1.Quantifiers.md)
# agda (for _cache/raw_agda_html/plfa.part2.Properties/src/plfa.part2.Properties.md)
# agda (for _cache/raw_agda_html/plfa.part1.Negation/src/plfa.part1.Negation.md)
# agda (for _cache/raw_agda_html/plfa.part1.Naturals/src/plfa.part1.Naturals.md)
# agda (for _cache/raw_agda_html/plfa.part2.More/src/plfa.part2.More.md)
# agda (for _cache/raw_agda_html/plfa.part1.Lists/src/plfa.part1.Lists.md)
# agda (for _cache/raw_agda_html/plfa.part2.Lambda/src/plfa.part2.Lambda.md)
# agda (for _cache/raw_agda_html/plfa.part1.Isomorphism/src/plfa.part1.Isomorphism.md)
# agda (for _cache/raw_agda_html/plfa.part2.Inference/src/plfa.part2.Inference.md)
# agda (for _cache/raw_agda_html/plfa.part1.Induction/src/plfa.part1.Induction.md)
# agda (for _cache/raw_agda_html/plfa.backmatter.Fonts/src/plfa.backmatter.Fonts.md)
# agda (for _cache/raw_agda_html/plfa.part1.Equality/src/plfa.part1.Equality.md)
# agda (for _cache/raw_agda_html/plfa.part3.Denotational/src/plfa.part3.Denotational.md)
# agda (for _cache/raw_agda_html/plfa.part1.Decidable/src/plfa.part1.Decidable.md)
# agda (for _cache/raw_agda_html/plfa.part2.DeBruijn/src/plfa.part2.DeBruijn.md)
# agda (for _cache/raw_agda_html/plfa.part3.ContextualEquivalence/src/plfa.part3.ContextualEquivalence.md)
# agda (for _cache/raw_agda_html/plfa.part1.Connectives/src/plfa.part1.Connectives.md)
# agda (for _cache/raw_agda_html/plfa.part2.Confluence/src/plfa.part2.Confluence.md)
# agda (for _cache/raw_agda_html/plfa.part3.Compositional/src/plfa.part3.Compositional.md)
# agda (for _cache/raw_agda_html/plfa.part2.Bisimulation/src/plfa.part2.Bisimulation.md)
# agda (for _cache/raw_agda_html/plfa.part2.BigStep/src/plfa.part2.BigStep.md)
# agda (for _cache/raw_agda_html/plfa.part3.Adequacy/src/plfa.part3.Adequacy.md)
# ebook-polish (for _site/plfa.epub)
Subsetting font: Frankenfont

------------------------------ REPORT ------------------------------
## Polishing: EPUB

### Inserting metadata jacket
Metadata jacket inserted

### Smartening punctuation
Smartened punctuation in: EPUB/text/ch004.xhtml
Smartened punctuation in: EPUB/text/ch006.xhtml
Smartened punctuation in: EPUB/text/ch007.xhtml
Smartened punctuation in: EPUB/text/ch017.xhtml
Smartened punctuation in: EPUB/text/ch023.xhtml
Smartened punctuation in: EPUB/text/ch024.xhtml
Smartened punctuation in: EPUB/text/ch025.xhtml
Smartened punctuation in: EPUB/text/ch027.xhtml
Smartened punctuation in: EPUB/text/ch030.xhtml
Smartened punctuation in: EPUB/text/ch031.xhtml
Smartened punctuation in: EPUB/text/ch033.xhtml
Smartened punctuation in: EPUB/text/ch036.xhtml

### Embedding referenced fonts
No embeddable fonts found

### Subsetting embedded fonts
Removed unused font: EPUB/fonts/mononoki-Bold.ttf
Removed unused font: EPUB/fonts/FreeMono-Bold.ttf
Removed unused font: EPUB/fonts/mononoki-Italic.ttf
Removed unused font: EPUB/fonts/DejaVuSans-Bold.ttf
Removed unused font: EPUB/fonts/mononoki-Regular.ttf
Removed unused font: EPUB/fonts/FreeMono-Regular.ttf
Removed unused font: EPUB/fonts/FreeMono-Oblique.ttf
Removed unused font: EPUB/fonts/DejaVuSerif-Bold.ttf
Removed unused font: EPUB/fonts/DejaVuMathTeXGyre.ttf
Removed unused font: EPUB/fonts/DejaVuSerif-Italic.ttf
Removed unused font: EPUB/fonts/DejaVuSans-Regular.ttf
Removed unused font: EPUB/fonts/DejaVuSans-Oblique.ttf
Removed unused font: EPUB/fonts/mononoki-BoldItalic.ttf
Decreased the font Frankenfont to 89.0% of its original size
Removed unused font: EPUB/fonts/DejaVuSerif-Regular.ttf
Removed unused font: EPUB/fonts/DejaVuSansMono-Bold.ttf
Removed unused font: EPUB/fonts/FreeMono-BoldOblique.ttf
Removed unused font: EPUB/fonts/DejaVuSans-ExtraLight.ttf
Removed unused font: EPUB/fonts/DejaVuSerif-BoldItalic.ttf
Removed unused font: EPUB/fonts/DejaVuSansMono-Regular.ttf
Removed unused font: EPUB/fonts/DejaVuSansMono-Oblique.ttf
Removed unused font: EPUB/fonts/DejaVuSans-BoldOblique.ttf
Removed unused font: EPUB/fonts/DejaVuSansMono-BoldOblique.ttf
Reduced total font size to 1.9% of original

### Removing unused CSS rules
Removed 365 unused CSS style rules
Removed 2 unused CSS selectors
No unused stylesheets found

### Upgrading book, if possible
No upgrade needed

### Adding soft hyphens
Soft hyphens added
----------------------------------------------------------------------
Polishing took: 5.9 seconds
Output written to: _site/plfa.epub
Build completed in 5m49s

331.78user 15.57system 5:49.65elapsed 99%CPU (0avgtext+0avgdata 2306944maxresident)k
4528inputs+697472outputs (46major+6677471minor)pagefaults 0swaps
nrnrnr commented 1 month ago

(For now, I am getting by with cabal v2-run builder _site/Confluence/index.html and similar.)

nrnrnr commented 1 month ago

Is it possible that make build is forcing git to change to the dev branch? Because I'm doing my development on another branch.

wenkokke commented 1 month ago

Is it possible that make build is forcing git to change to the dev branch? Because I'm doing my development on another branch.

I don't think so.

wadler commented 1 month ago

Yes, that is a problem. Fixing it takes resources, and I'm encouraging Wen to finish her dissertation rather than to improve PLFA. Go well, – P