From 25fa65209437417ee1afd4634618b07460a2e327 Mon Sep 17 00:00:00 2001 From: zeme Date: Thu, 24 Apr 2025 13:47:31 +0200 Subject: [PATCH 1/5] Simplify Latex Builds --- doc/cost-model-overview/Makefile | 35 ++---------- doc/extended-utxo-spec/Makefile | 48 ++--------------- doc/notes/cost-model-notes/Makefile | 42 ++------------- .../fomega/cek-cps-experiments/tex/Makefile | 9 ++-- doc/notes/fomega/lazy-machine/Makefile | 42 ++------------- doc/papers/eutxoma/Makefile | 48 ++--------------- doc/papers/system-f-in-agda/Makefile | 46 ++-------------- doc/papers/utxoma/Makefile | 48 ++--------------- doc/plutus-core-spec-old/Makefile | 46 ++-------------- .../{latexmkrc => .latexmkrc} | 0 doc/plutus-core-spec/Makefile | 50 ++--------------- doc/plutus-core-spec/figures/Makefile | 5 -- doc/plutus-report/Makefile | 5 ++ nix/build-latex-doc.nix | 49 ++++++++++++----- nix/build-latex.nix | 51 ------------------ nix/latex-documents.nix | 26 +++++---- nix/outputs.nix | 9 +--- nix/unraveling-recursion-paper.nix | 54 ------------------- 18 files changed, 87 insertions(+), 526 deletions(-) rename doc/plutus-core-spec/{latexmkrc => .latexmkrc} (100%) delete mode 100644 doc/plutus-core-spec/figures/Makefile create mode 100644 doc/plutus-report/Makefile delete mode 100644 nix/build-latex.nix delete mode 100644 nix/unraveling-recursion-paper.nix diff --git a/doc/cost-model-overview/Makefile b/doc/cost-model-overview/Makefile index d38c48ab70b..562357d466e 100644 --- a/doc/cost-model-overview/Makefile +++ b/doc/cost-model-overview/Makefile @@ -1,35 +1,6 @@ -DOC=cost-model-overview - -PDF=${DOC}.pdf -BIB=${DOC}.bib - -SRC = ${DOC}.tex - -LATEX = pdflatex -halt-on-error -shell-escape - -.PHONEY: all pdf again clean - -#---------------------------------------------------------------- - -all: pdf - -pdf: ${PDF} - -${DOC}.pdf: ${SRC} - -rm -f ${DOC}.bbl ${DOC}.aux ${DOC}.nls ${DOC}.nlo - ${LATEX} ${DOC} - ${LATEX} ${DOC} # to make sure the (cross)references are correct - ${LATEX} ${DOC} - -#---------------------------------------------------------------- -again: - touch ${DOC}.tex && ${MAKE} +all: + latexmk -pdf cost-model-overview.tex clean: - rm -f *.aux *.log *.cov *.par *.bbl *.fls *.blg *.out *.xml *.bcf *.dvi *.toc *.tdo *.nls *.nlo *.ilg *~ - -clean2: clean - rm -f ${DOC}.pdf + latexmk -C -v: ${PDF} - ${PDFVIEWER} ${PDF} 2>/dev/null & diff --git a/doc/extended-utxo-spec/Makefile b/doc/extended-utxo-spec/Makefile index 39f1e695650..74acaa88562 100644 --- a/doc/extended-utxo-spec/Makefile +++ b/doc/extended-utxo-spec/Makefile @@ -1,46 +1,6 @@ -DOC=extended-utxo-specification +all: + latexmk -pdf extended-utxo-specification.tex -PDF=${DOC}.pdf -BIB=${DOC}.bib - -FIGS=./figures - -SRC = ${DOC}.tex ${BIB} - - -LATEX = pdflatex -halt-on-error -shell-escape # To get pstricks to work with PDF -BIBTEX = bibtex - -.PHONEY: all pdf figs again clean - -#---------------------------------------------------------------- - -all: pdf - -pdf: ${PDF} - -${DOC}.pdf: ${SRC} - rm -f ${DOC}.bbl - ${LATEX} ${DOC} - ${BIBTEX} ${DOC} - ${LATEX} ${DOC} # to make sure the (cross)references are correct - ${LATEX} ${DOC} - ${LATEX} ${DOC} - -figs: - cd ${FIGS} && ${MAKE} - -#---------------------------------------------------------------- -again: - touch ${DOC}.tex && ${MAKE} - -clean1: - rm -f *.aux *.log *.cov *.par *.bbl *.fls *.blg *.xml *.bcf *.dvi *~ - cd ${FIGS} && ${MAKE} clean - -clean: clean1 - rm -f ${DOC}.pdf - -v: ${PDF} - acroread ${PDF} 2>/dev/null +clean: + latexmk -C diff --git a/doc/notes/cost-model-notes/Makefile b/doc/notes/cost-model-notes/Makefile index ff73979d796..1e469f29f00 100644 --- a/doc/notes/cost-model-notes/Makefile +++ b/doc/notes/cost-model-notes/Makefile @@ -1,42 +1,6 @@ -DOC=cost-model-notes - -PDF=${DOC}.pdf - -FIGS=./figures - -SRC = ${DOC}.tex - - -LATEX = pdflatex -halt-on-error -shell-escape - -.PHONEY: all pdf figs again clean - -#---------------------------------------------------------------- - -all: pdf - -pdf: ${PDF} - -${DOC}.pdf: ${SRC} - -rm -f ${DOC}.bbl ${DOC}.aux - ${LATEX} ${DOC} - ${LATEX} ${DOC} - ${LATEX} ${DOC} - -figs: - cd ${FIGS} && ${MAKE} - -#---------------------------------------------------------------- -again: - touch ${DOC}.tex && ${MAKE} +all: + latexmk -pdf cost-model-nodes.tex clean: - rm -f *.aux *.log *.cov *.par *.bbl *.fls *.blg *.xml *.bcf *.dvi *~ - cd ${FIGS} && ${MAKE} clean - -clean2: clean - rm -f ${DOC}.pdf - -v: ${PDF} - acroread ${PDF} 2>/dev/null & + latexmk -C diff --git a/doc/notes/fomega/cek-cps-experiments/tex/Makefile b/doc/notes/fomega/cek-cps-experiments/tex/Makefile index 527393dc853..fd469633fd0 100644 --- a/doc/notes/fomega/cek-cps-experiments/tex/Makefile +++ b/doc/notes/fomega/cek-cps-experiments/tex/Makefile @@ -1,9 +1,6 @@ -all: results.pdf - -results.pdf: results.tex - pdflatex results.tex - pdflatex results.tex +all: + latexmk -pdf results.tex clean: - -rm -f *.log *.aux *~ + latexmk -C diff --git a/doc/notes/fomega/lazy-machine/Makefile b/doc/notes/fomega/lazy-machine/Makefile index 1e85151ed32..82e6da5b1ca 100644 --- a/doc/notes/fomega/lazy-machine/Makefile +++ b/doc/notes/fomega/lazy-machine/Makefile @@ -1,42 +1,6 @@ -DOC=lazy-plutus-core -PDF=${DOC}.pdf -BIB=${DOC}.bib - -SRC = ${DOC}.tex ckmachine.tex cekmachine.tex lmachine.tex ${BIB} - - -FIGS=./figs - -LATEX = pdflatex -halt-on-error -shell-escape # To get pstricks to work with PDF -BIBTEX = bibtex - -.PHONEY: all pdf v clean # figs pngs - -#---------------------------------------------------------------- - -all: pdf - -pdf: ${PDF} - -${DOC}.pdf: ${SRC} ${BIB} - ${LATEX} ${DOC} - ${BIBTEX} ${DOC} - ${LATEX} ${DOC} # to make sure the (cross)references are correct - ${LATEX} ${DOC} - -figs: - cd ${FIGS} && ${MAKE} - -pngs: - cd ${FIGS} && ${MAKE} pngs -#---------------------------------------------------------------- - -v: ${DOC}.pdf - acroread ${DOC}.pdf +all: + latexmk -pdf lazy-plutus-core.tex clean: - rm -f *.aux *.log *.cov *.par *.bbl *.fls *.blg *.xml *.bcf *~ -# cd ${FIGS} && ${MAKE} clean + latexmk -C -clean2: - ${MAKE} clean && rm -rf ${PDF} diff --git a/doc/papers/eutxoma/Makefile b/doc/papers/eutxoma/Makefile index c394d8faa30..4ff0afa80f0 100644 --- a/doc/papers/eutxoma/Makefile +++ b/doc/papers/eutxoma/Makefile @@ -1,45 +1,5 @@ -DOC=eutxoma - -PDF=${DOC}.pdf -BIB=${DOC}.bib - -FIGS=./figures - -SRC = *.tex ${BIB} - - -LATEX = pdflatex -halt-on-error -shell-escape # To get pstricks to work with PDF -BIBTEX = bibtex - -.PHONEY: all pdf figs again clean - -#---------------------------------------------------------------- - -all: pdf - -pdf: ${PDF} - -${DOC}.pdf: ${SRC} - rm -f ${DOC}.bbl - ${LATEX} ${DOC} - ${BIBTEX} ${DOC} - ${LATEX} ${DOC} # to make sure the (cross)references are correct - ${LATEX} ${DOC} - -figs: -# cd ${FIGS} && ${MAKE} - -#---------------------------------------------------------------- -again: - touch ${DOC}.tex && ${MAKE} - -clean1: - rm -f *.aux *.log *.cov *.par *.bbl *.fls *.blg *.xml *.bcf *.dvi *.out *~ -# cd ${FIGS} && ${MAKE} clean - -clean: clean1 - rm -f ${DOC}.pdf - -v: ${PDF} - acroread 2>/dev/null ${PDF} +all: + latexmk -pdf eutxoma.tex +clean: + latexmk -C diff --git a/doc/papers/system-f-in-agda/Makefile b/doc/papers/system-f-in-agda/Makefile index c97efd3cd8a..b5aaee8f3d4 100644 --- a/doc/papers/system-f-in-agda/Makefile +++ b/doc/papers/system-f-in-agda/Makefile @@ -1,45 +1,7 @@ -DOC=paper -BIBFILE =bibliography -PDF=${DOC}.pdf -BIB=${BIBFILE}.bib - -LAGDA = ${DOC}.lagda -SRC = ${DOC}.tex ${BIB} - -AGDA = agda --latex --latex-dir . -LATEX = pdflatex -halt-on-error -shell-escape # To get pstricks to work with PDF -BIBTEX = bibtex - -.PHONEY: all pdf figs again clean - -#---------------------------------------------------------------- - -all: pdf - -pdf: ${PDF} - -${DOC}.pdf: ${LAGDA} - ${AGDA} ${LAGDA} - ${LATEX} ${DOC} - ${BIBTEX} ${DOC} - ${LATEX} ${DOC} # to make sure the (cross)references are correct - ${LATEX} ${DOC} - -figs: - cd ${FIGS} && ${MAKE} - - -#---------------------------------------------------------------- - -again: - touch ${DOC}.lagda && ${MAKE} +all: + agda --latex --latex-dir . + latexmk -pdf system-f-in-agda.tex clean: - rm -f ${DOC}.tex *.aux *.log *.cov *.par *.bbl *.fls *.blg *.xml *.bcf *.dvi *.out *~ - -clean2: clean - rm -f ${DOC}.pdf - -v: ${PDF} - acroread ${PDF} + latexmk -C diff --git a/doc/papers/utxoma/Makefile b/doc/papers/utxoma/Makefile index 77c9b8110a0..89a1c859aa1 100644 --- a/doc/papers/utxoma/Makefile +++ b/doc/papers/utxoma/Makefile @@ -1,45 +1,5 @@ -DOC=utxoma - -PDF=${DOC}.pdf -BIB=${DOC}.bib - -FIGS=./figures - -SRC = *.tex ${BIB} - - -LATEX = pdflatex -halt-on-error -shell-escape # To get pstricks to work with PDF -BIBTEX = bibtex - -.PHONEY: all pdf figs again clean - -#---------------------------------------------------------------- - -all: pdf - -pdf: ${PDF} - -${DOC}.pdf: ${SRC} - rm -f ${DOC}.bbl - ${LATEX} ${DOC} - ${BIBTEX} ${DOC} - ${LATEX} ${DOC} # to make sure the (cross)references are correct - ${LATEX} ${DOC} - -figs: -# cd ${FIGS} && ${MAKE} - -#---------------------------------------------------------------- -again: - touch ${DOC}.tex && ${MAKE} - -clean1: - rm -f *.aux *.log *.cov *.par *.bbl *.fls *.blg *.xml *.bcf *.dvi *.out *~ -# cd ${FIGS} && ${MAKE} clean - -clean: clean1 - rm -f ${DOC}.pdf - -v: ${PDF} - acroread 2>/dev/null ${PDF} +all: + latexmk -pdf utxoma.tex +clean: + latexmk -C diff --git a/doc/plutus-core-spec-old/Makefile b/doc/plutus-core-spec-old/Makefile index 656a4b449c0..bf5c664b1a1 100644 --- a/doc/plutus-core-spec-old/Makefile +++ b/doc/plutus-core-spec-old/Makefile @@ -1,46 +1,6 @@ -DOC=plutus-core-specification - -PDF=${DOC}.pdf -BIB=${DOC}.bib - -FIGS=./figures - -SRC = ${DOC}.tex ${BIB} ${FIGS}/*.tex - - -LATEX = pdflatex -halt-on-error -shell-escape # To get pstricks to work with PDF -BIBTEX = bibtex - -.PHONEY: all pdf figs again clean - -#---------------------------------------------------------------- - -all: pdf - -pdf: ${PDF} - -${DOC}.pdf: ${SRC} - -rm -f ${DOC}.bbl ${DOC}.aux - ${LATEX} ${DOC} - ${BIBTEX} ${DOC} - ${LATEX} ${DOC} # to make sure the (cross)references are correct - ${LATEX} ${DOC} - ${LATEX} ${DOC} - -figs: - cd ${FIGS} && ${MAKE} - -#---------------------------------------------------------------- -again: - touch ${DOC}.tex && ${MAKE} +all: + latexmk -pdf plutus-core-specification.tex clean: - rm -f *.aux *.log *.cov *.par *.bbl *.fls *.blg *.xml *.bcf *.dvi *.out *~ - cd ${FIGS} && ${MAKE} clean - -clean2: clean - rm -f ${DOC}.pdf - -v: ${PDF} - acroread ${PDF} 2>/dev/null & + latexmk -C diff --git a/doc/plutus-core-spec/latexmkrc b/doc/plutus-core-spec/.latexmkrc similarity index 100% rename from doc/plutus-core-spec/latexmkrc rename to doc/plutus-core-spec/.latexmkrc diff --git a/doc/plutus-core-spec/Makefile b/doc/plutus-core-spec/Makefile index 25ebf1cc5e2..96433679a51 100644 --- a/doc/plutus-core-spec/Makefile +++ b/doc/plutus-core-spec/Makefile @@ -1,49 +1,5 @@ -DOC=plutus-core-specification - -PDF=${DOC}.pdf -BIB=${DOC}.bib - -FIGS=./figures - -SRC = *.tex cardano/*.tex ${BIB} # ${FIGS}/*.tex - - -LATEX = pdflatex -halt-on-error -shell-escape # To get pstricks to work with PDF -BIBTEX = bibtex -MAKEINDEX = makeindex - -.PHONEY: all pdf figs again clean - -#---------------------------------------------------------------- - -all: pdf - -pdf: ${PDF} - -${DOC}.pdf: ${SRC} ${BIB} - -rm -f ${DOC}.bbl ${DOC}.aux ${DOC}.nls ${DOC}.nlo - ${LATEX} ${DOC} - ${BIBTEX} ${DOC} - ${LATEX} ${DOC} # to make sure the (cross)references are correct - ${MAKEINDEX} ${DOC}.nlo -s nomencl.ist -o ${DOC}.nls - ${LATEX} ${DOC} - ${MAKEINDEX} ${DOC}.nlo -s nomencl.ist -o ${DOC}.nls - ${LATEX} ${DOC} - ${MAKEINDEX} ${DOC}.nlo -s nomencl.ist -o ${DOC}.nls - ${LATEX} ${DOC} - -figs: - cd ${FIGS} && ${MAKE} - -#---------------------------------------------------------------- -again: - touch ${DOC}.tex && ${MAKE} +all: + latexmk -pdf plutus-core-specification.tex clean: - rm -f *.aux *.log *.cov *.par *.bbl *.fls *.blg *.out *.xml *.bcf *.dvi *.toc *.tdo *.nls *.nlo *.ilg *~ - -clean2: clean - rm -f ${DOC}.pdf - -v: ${PDF} - ${PDFVIEWER} ${PDF} 2>/dev/null & + latexmk -C diff --git a/doc/plutus-core-spec/figures/Makefile b/doc/plutus-core-spec/figures/Makefile deleted file mode 100644 index 28888788968..00000000000 --- a/doc/plutus-core-spec/figures/Makefile +++ /dev/null @@ -1,5 +0,0 @@ -# No figures yet! -all: - -clean: - diff --git a/doc/plutus-report/Makefile b/doc/plutus-report/Makefile new file mode 100644 index 00000000000..bfadc07e791 --- /dev/null +++ b/doc/plutus-report/Makefile @@ -0,0 +1,5 @@ +all: + latexmk -pdf plutus.tex + +clean: + latexmk -C diff --git a/nix/build-latex-doc.nix b/nix/build-latex-doc.nix index 051029bbc3d..bcfa3154fec 100644 --- a/nix/build-latex-doc.nix +++ b/nix/build-latex-doc.nix @@ -1,15 +1,33 @@ -{ pkgs, lib, agda-tools, build-latex }: +{ pkgs, lib, agda-tools }: -{ name, description, src, texFiles ? null, withAgda ? false, agdaFile ? "" }: +{ name, description, src, texFile ? null, agdaFile ? null }: -build-latex { +let + + latexEnvironment = pkgs.texlive.combine { + inherit (pkgs.texlive) + acmart + bibtex + biblatex + collection-bibtexextra + collection-fontsextr + collection-fontsrecommended + collection-latex + collection-latexextr + collection-luatex + collection-mathscience scheme-small + latexmk; + }; + + agdaInputs = lib.optionals (agdaFile != null) [ agda-tools.agda-with-stdlib ]; + +in + +pkgs.stdenv.mkDerivation { inherit name; inherit description; - inherit texFiles; - # A typical good filter for latex sources. - # This also includes files for cases where agda sources are being compiled. src = lib.sourceFilesBySuffices src [ ".tex" ".bib" @@ -20,18 +38,21 @@ build-latex { ".agda" ".agda-lib" ".lagda" + ".md" + ".latexmkrc" + "Makefile" ]; - buildInputs = lib.optionals withAgda [ agda-tools.agda-with-stdlib ]; + buildInputs = agdaInputs ++ [ latexEnvironment pkgs.zip ]; - texInputs = { - inherit (pkgs.texlive) - acmart bibtex biblatex collection-bibtexextra collection-fontsextra - collection-fontsrecommended collection-latex collection-latexextra - collection-luatex collection-mathscience scheme-small; - }; + phases = [ "buildPhase" ]; + + buildPhase = '' + make + cp *.pdf $out + ''; - preBuild = lib.optionalString withAgda '' + preBuild = lib.optionalString (agdaFile != null) '' agda-with-stdlib --latex ${agdaFile} --latex-dir . ''; diff --git a/nix/build-latex.nix b/nix/build-latex.nix deleted file mode 100644 index adb1ea37df1..00000000000 --- a/nix/build-latex.nix +++ /dev/null @@ -1,51 +0,0 @@ -{ pkgs }: - -# Build a latex derivation using latexmk. -{ texFiles ? [ ] -, # The specific tex files to build, will try and build all of them if absent - texInputs ? { inherit (pkgs.texlive) scheme-small; } -, # Tex dependencies as an attrset - buildInputs ? [ ] -, # Additional build inputs - ... -}@attrs: - -let - tex = pkgs.texlive.combine (texInputs // { inherit (pkgs.texlive) latexmk; }); - - # mkDerivation doesn't like having this as an attr, and we don't need to pass it through - filteredAttrs = builtins.removeAttrs attrs [ "texInputs" ]; - - buildDir = ".nix-build"; - -in -pkgs.stdenv.mkDerivation (filteredAttrs // { - - buildInputs = [ tex ] ++ buildInputs; - - buildPhase = '' - runHook preBuild - mkdir -p ${buildDir} - # The bibtex_fudge setting is because our version of latexmk has an issue with bibtex - # and explicit output directories, which should be fixed in v4.70b: - # https://tex.stackexchange.com/questions/564626/latexmk-4-70a-doesnt-compile-document-with-bibtex-citation # editorconfig-checker-disable-line - latexmk \ - -e '$bibtex_fudge=1' \ - -outdir=${buildDir} \ - -pdf \ - ${toString texFiles} - runHook postBuild - ''; - - installPhase = '' - runHook preInstall - mkdir -p $out - install -t $out ${buildDir}/*.pdf - - mkdir -p $out/nix-support - for pdf in $out/*.pdf; do - echo "doc-pdf $(basename $pdf .pdf) $pdf" >> $out/nix-support/hydra-build-products - done - runHook postInstall - ''; -}) diff --git a/nix/latex-documents.nix b/nix/latex-documents.nix index 07fca6aac77..9d6d7a55f45 100644 --- a/nix/latex-documents.nix +++ b/nix/latex-documents.nix @@ -2,42 +2,38 @@ { cost-model-notes = build-latex-doc { name = "cost-model-notes"; - src = self + /doc/notes/cost-model-notes; description = "Notes on cost models"; - texFiles = [ "cost-model-notes.tex" ]; + src = self + /doc/notes/cost-model-notes; }; eutxo-paper = build-latex-doc { name = "eutxo-paper"; description = "eutxo"; src = self + /doc/papers/eutxo; - texFiles = [ "eutxo.tex" ]; }; eutxoma-paper = build-latex-doc { name = "eutxoma-paper"; description = "eutxoma"; src = self + /doc/papers/eutxoma; - texFiles = [ "eutxoma.tex" ]; }; extended-utxo-spec = build-latex-doc { name = "extended-utxo-spec"; - src = self + /doc/extended-utxo-spec; description = "Extended UTXO specification"; + src = self + /doc/extended-utxo-spec; }; lazy-machine-notes = build-latex-doc { name = "lazy-machine-notes"; - src = self + /doc/notes/fomega/lazy-machine; - texFiles = [ "lazy-plutus-core.tex" ]; description = "lazy machine discussion"; + src = self + /doc/notes/fomega/lazy-machine; }; multi-currency-notes = build-latex-doc { name = "multi-currency-notes"; - src = self + /doc/notes/multi-currency; description = "Multi-currency paper"; + src = self + /doc/notes/multi-currency; }; plutus-core-spec-old = build-latex-doc { @@ -50,22 +46,18 @@ name = "plutus-core-spec"; description = "Plutus core specification"; src = self + /doc/plutus-core-spec; - texFiles = [ "plutus-core-specification.tex" ]; }; plutus-report = build-latex-doc { name = "plutus-report"; description = "plutus report"; src = self + /doc/plutus-report; - texFiles = [ "plutus.tex" ]; }; system-f-in-agda-paper = build-latex-doc { name = "system-f-in-agda-paper"; - src = self + /doc/papers/system-f-in-agda; description = "system-f in agda"; - texFiles = [ "paper.tex" ]; - withAgda = true; + src = self + /doc/papers/system-f-in-agda; agdaFile = "paper.lagda"; }; @@ -73,6 +65,12 @@ name = "utxoma-paper"; description = "utxoma"; src = self + /doc/papers/utxoma; - texFiles = [ "utxoma.tex" ]; + }; + + unraveling-recursion-paper = build-latex-doc { + name = "unraveling-recursion-paper"; + description = "unraveling recursion-paper"; + src = self + /doc/papers/unraveling-recursion; + agdaFile = "paper.lagda"; }; } diff --git a/nix/outputs.nix b/nix/outputs.nix index 4fa0d80eb39..14996afa6bf 100644 --- a/nix/outputs.nix +++ b/nix/outputs.nix @@ -11,9 +11,6 @@ let utils = import ./utils.nix { inherit lib; }; - build-latex = import ./build-latex.nix - { inherit pkgs; }; - r-with-packages = import ./r-with-packages.nix { inherit pkgs; }; @@ -24,10 +21,7 @@ let { inherit self pkgs lib metatheory-agda-library; }; build-latex-doc = import ./build-latex-doc.nix - { inherit pkgs lib agda-tools build-latex; }; - - unraveling-recursion-paper = import ./unraveling-recursion-paper.nix - { inherit self pkgs lib build-latex agda-tools; }; + { inherit pkgs lib agda-tools; }; latex-documents = import ./latex-documents.nix { inherit self build-latex-doc; }; @@ -65,7 +59,6 @@ let }; extra-artifacts = - { inherit unraveling-recursion-paper; } // { inherit metatheory-site; } // { inherit metatheory-agda-library; } // (latex-documents); diff --git a/nix/unraveling-recursion-paper.nix b/nix/unraveling-recursion-paper.nix deleted file mode 100644 index 53c196c469b..00000000000 --- a/nix/unraveling-recursion-paper.nix +++ /dev/null @@ -1,54 +0,0 @@ -{ self, pkgs, lib, build-latex, agda-tools }: - -let - artifacts = pkgs.runCommand "FIR-compiler" - { - buildInputs = [ pkgs.zip ]; - src = self + /doc/papers/unraveling-recursion/code; - } '' - mkdir -p $out - cd $src - zip -r $out/compiler.zip . - ''; - -in - -build-latex { - name = "unraveling-recursion-paper"; - - texFiles = [ "unraveling-recursion.tex" ]; - - texInputs = { - # more than we need at the moment, but doesn't cost much to include it - inherit (pkgs.texlive) - scheme-small collection-bibtexextra collection-latex collection-latexextra - collection-luatex collection-fontsextra collection-fontsrecommended - collection-mathscience acmart bibtex biblatex; - }; - - buildInputs = [ agda-tools.agda-with-stdlib pkgs.zip ]; - - src = - lib.sourceFilesBySuffices (self + /doc/papers/unraveling-recursion) [ - ".tex" - ".bib" - ".agda" - ".lagda" - ".cls" - ".bst" - ".pdf" - ]; - - preBuild = '' - for file in *.lagda; do - agda-with-stdlib --latex $file --latex-dir . - done - - echo "\toggletrue{lagda}" > agdaswitch.tex - ''; - - postInstall = '' - cp ${artifacts}/* $out - zip -r $out/sources.zip *.tex *.bib *.cls *.bst *.bbl *.sty copyright-form.pdf - ''; -} From 535307b9770c68d5fa05cc47049c14f2f7e6dec1 Mon Sep 17 00:00:00 2001 From: zeme Date: Thu, 24 Apr 2025 14:47:57 +0200 Subject: [PATCH 2/5] Simplify LaTeX Builds --- .gitignore | 1 + doc/extended-utxo-spec/Makefile | 2 +- doc/notes/cost-model-notes/Makefile | 4 +- doc/notes/fomega/lazy-machine/Makefile | 2 +- doc/notes/multi-currency/Makefile | 6 +++ doc/papers/eutxo/Makefile | 6 +++ doc/papers/eutxoma/Makefile | 3 +- doc/papers/system-f-in-agda/.gitignore | 2 + doc/papers/system-f-in-agda/Makefile | 4 +- .../{paper.lagda => system-f-in-agda.lagda} | 0 doc/papers/unraveling-recursion/.gitignore | 4 ++ doc/papers/unraveling-recursion/Makefile | 8 ++++ .../unraveling-recursion/agdaswitch.tex | 1 + doc/papers/utxoma/Makefile | 2 +- doc/plutus-core-spec-old/Makefile | 2 +- doc/plutus-core-spec/.latexmkrc | 2 +- doc/plutus-core-spec/Makefile | 2 +- doc/plutus-report/Makefile | 2 +- nix/build-latex-doc.nix | 46 +++++++++---------- nix/latex-documents.nix | 12 ++--- 20 files changed, 69 insertions(+), 42 deletions(-) create mode 100644 doc/notes/multi-currency/Makefile create mode 100644 doc/papers/eutxo/Makefile rename doc/papers/system-f-in-agda/{paper.lagda => system-f-in-agda.lagda} (100%) create mode 100644 doc/papers/unraveling-recursion/Makefile create mode 100644 doc/papers/unraveling-recursion/agdaswitch.tex diff --git a/.gitignore b/.gitignore index 6bec936487f..f1a61d3704a 100644 --- a/.gitignore +++ b/.gitignore @@ -108,6 +108,7 @@ linkchecker-out.txt plutus-pab/test-node/testnet/db plutus-pab/test-node/alonzo-purple/db *.actual.json +*.sty # profiling output files *.timelog *.stacks diff --git a/doc/extended-utxo-spec/Makefile b/doc/extended-utxo-spec/Makefile index 74acaa88562..9690cd65b88 100644 --- a/doc/extended-utxo-spec/Makefile +++ b/doc/extended-utxo-spec/Makefile @@ -2,5 +2,5 @@ all: latexmk -pdf extended-utxo-specification.tex clean: - latexmk -C + latexmk -C && rm -f *.bbl *.nlo *.nls *.ist *.thm diff --git a/doc/notes/cost-model-notes/Makefile b/doc/notes/cost-model-notes/Makefile index 1e469f29f00..c12dcf09401 100644 --- a/doc/notes/cost-model-notes/Makefile +++ b/doc/notes/cost-model-notes/Makefile @@ -1,6 +1,6 @@ all: - latexmk -pdf cost-model-nodes.tex + latexmk -pdf cost-model-notes.tex clean: - latexmk -C + latexmk -C && rm -f *.bbl *.nlo *.nls *.ist *.thm diff --git a/doc/notes/fomega/lazy-machine/Makefile b/doc/notes/fomega/lazy-machine/Makefile index 82e6da5b1ca..e948feb6648 100644 --- a/doc/notes/fomega/lazy-machine/Makefile +++ b/doc/notes/fomega/lazy-machine/Makefile @@ -2,5 +2,5 @@ all: latexmk -pdf lazy-plutus-core.tex clean: - latexmk -C + latexmk -C && rm -f *.bbl *.nlo *.nls *.ist *.thm diff --git a/doc/notes/multi-currency/Makefile b/doc/notes/multi-currency/Makefile new file mode 100644 index 00000000000..db4ba5b7c6a --- /dev/null +++ b/doc/notes/multi-currency/Makefile @@ -0,0 +1,6 @@ +all: + latexmk -pdf main.tex + +clean: + latexmk -C && rm -f *.bbl *.nlo *.nls *.ist *.thm + diff --git a/doc/papers/eutxo/Makefile b/doc/papers/eutxo/Makefile new file mode 100644 index 00000000000..ce167733f3e --- /dev/null +++ b/doc/papers/eutxo/Makefile @@ -0,0 +1,6 @@ +all: + latexmk -pdf eutxo.tex + +clean: + latexmk -C && rm -f *.bbl *.nlo *.nls *.ist *.thm + diff --git a/doc/papers/eutxoma/Makefile b/doc/papers/eutxoma/Makefile index 4ff0afa80f0..27812084a87 100644 --- a/doc/papers/eutxoma/Makefile +++ b/doc/papers/eutxoma/Makefile @@ -2,4 +2,5 @@ all: latexmk -pdf eutxoma.tex clean: - latexmk -C + latexmk -C && rm -f *.bbl *.nlo *.nls *.ist *.thm + diff --git a/doc/papers/system-f-in-agda/.gitignore b/doc/papers/system-f-in-agda/.gitignore index a1363379944..405121e2649 100644 --- a/doc/papers/system-f-in-agda/.gitignore +++ b/doc/papers/system-f-in-agda/.gitignore @@ -1 +1,3 @@ *.pdf +# Generated by agda +system-f-in-agda.tex \ No newline at end of file diff --git a/doc/papers/system-f-in-agda/Makefile b/doc/papers/system-f-in-agda/Makefile index b5aaee8f3d4..30dcc522714 100644 --- a/doc/papers/system-f-in-agda/Makefile +++ b/doc/papers/system-f-in-agda/Makefile @@ -1,7 +1,7 @@ all: - agda --latex --latex-dir . + agda-with-stdlib --latex system-f-in-agda.lagda --latex-dir . latexmk -pdf system-f-in-agda.tex clean: - latexmk -C + latexmk -C && rm -f *.bbl *.nlo *.nls *.ist *.thm *.sty *.ptb diff --git a/doc/papers/system-f-in-agda/paper.lagda b/doc/papers/system-f-in-agda/system-f-in-agda.lagda similarity index 100% rename from doc/papers/system-f-in-agda/paper.lagda rename to doc/papers/system-f-in-agda/system-f-in-agda.lagda diff --git a/doc/papers/unraveling-recursion/.gitignore b/doc/papers/unraveling-recursion/.gitignore index a02e55ecce2..67d88f76ba3 100644 --- a/doc/papers/unraveling-recursion/.gitignore +++ b/doc/papers/unraveling-recursion/.gitignore @@ -1,2 +1,6 @@ *.pdf latex +# Generated by agda +IFix.tex +RecursiveData.tex +RecursiveTerms.tex \ No newline at end of file diff --git a/doc/papers/unraveling-recursion/Makefile b/doc/papers/unraveling-recursion/Makefile new file mode 100644 index 00000000000..b78cf2a3707 --- /dev/null +++ b/doc/papers/unraveling-recursion/Makefile @@ -0,0 +1,8 @@ +all: + for f in *.lagda; do \ + agda-with-stdlib --latex $$f --latex-dir .; \ + done + latexmk -pdf unraveling-recursion.tex + +clean: + latexmk -C && rm -f *.bbl *.nlo *.nls *.ist *.thm *.sty *.ptb *.agdai \ No newline at end of file diff --git a/doc/papers/unraveling-recursion/agdaswitch.tex b/doc/papers/unraveling-recursion/agdaswitch.tex new file mode 100644 index 00000000000..9b3d63ff166 --- /dev/null +++ b/doc/papers/unraveling-recursion/agdaswitch.tex @@ -0,0 +1 @@ +\toggletrue{lagda} diff --git a/doc/papers/utxoma/Makefile b/doc/papers/utxoma/Makefile index 89a1c859aa1..41874a1968f 100644 --- a/doc/papers/utxoma/Makefile +++ b/doc/papers/utxoma/Makefile @@ -2,4 +2,4 @@ all: latexmk -pdf utxoma.tex clean: - latexmk -C + latexmk -C && rm -f *.bbl *.nlo *.nls *.ist *.thm diff --git a/doc/plutus-core-spec-old/Makefile b/doc/plutus-core-spec-old/Makefile index bf5c664b1a1..3354dd130d7 100644 --- a/doc/plutus-core-spec-old/Makefile +++ b/doc/plutus-core-spec-old/Makefile @@ -2,5 +2,5 @@ all: latexmk -pdf plutus-core-specification.tex clean: - latexmk -C + latexmk -C && rm -f *.bbl *.nlo *.nls *.ist *.thm diff --git a/doc/plutus-core-spec/.latexmkrc b/doc/plutus-core-spec/.latexmkrc index 4588f494156..31477171d57 100644 --- a/doc/plutus-core-spec/.latexmkrc +++ b/doc/plutus-core-spec/.latexmkrc @@ -1,5 +1,5 @@ # Custom dependency and function for nomencl package add_cus_dep( 'nlo', 'nls', 0, 'makenlo2nls' ); sub makenlo2nls { - system( "makeindex -s nomencl.ist -o \"$_[0].nls\" \"$_[0].nlo\"" ); + system( "makeindex -s nomencl.ist -o \"$_[0].nls\" \"$_[0].nlo\"" ); } diff --git a/doc/plutus-core-spec/Makefile b/doc/plutus-core-spec/Makefile index 96433679a51..65706b1a136 100644 --- a/doc/plutus-core-spec/Makefile +++ b/doc/plutus-core-spec/Makefile @@ -2,4 +2,4 @@ all: latexmk -pdf plutus-core-specification.tex clean: - latexmk -C + latexmk -C && rm -f *.bbl *.nlo *.nls *.ist *.thm diff --git a/doc/plutus-report/Makefile b/doc/plutus-report/Makefile index bfadc07e791..9962942d157 100644 --- a/doc/plutus-report/Makefile +++ b/doc/plutus-report/Makefile @@ -2,4 +2,4 @@ all: latexmk -pdf plutus.tex clean: - latexmk -C + latexmk -C && rm -f *.bbl *.nlo *.nls *.ist *.thm \ No newline at end of file diff --git a/nix/build-latex-doc.nix b/nix/build-latex-doc.nix index bcfa3154fec..55c3be2a9cb 100644 --- a/nix/build-latex-doc.nix +++ b/nix/build-latex-doc.nix @@ -1,26 +1,24 @@ -{ pkgs, lib, agda-tools }: +{ pkgs, lib }: -{ name, description, src, texFile ? null, agdaFile ? null }: +{ name, description, src }: let - latexEnvironment = pkgs.texlive.combine { - inherit (pkgs.texlive) - acmart - bibtex - biblatex - collection-bibtexextra - collection-fontsextr - collection-fontsrecommended - collection-latex - collection-latexextr - collection-luatex - collection-mathscience scheme-small - latexmk; - }; - - agdaInputs = lib.optionals (agdaFile != null) [ agda-tools.agda-with-stdlib ]; - + latexEnvironment = pkgs.texliveFull; + # pkgs.texlive.combine { + # inherit (pkgs.texlive) + # acmart + # bibtex + # biblatex + # collection-bibtexextra + # collection-fontsextr + # collection-fontsrecommended + # collection-latex + # collection-latexextr + # collection-luatex + # collection-mathscience scheme-small + # latexmk; + # }; in pkgs.stdenv.mkDerivation { @@ -43,7 +41,11 @@ pkgs.stdenv.mkDerivation { "Makefile" ]; - buildInputs = agdaInputs ++ [ latexEnvironment pkgs.zip ]; + buildInputs = [ + latexEnvironment + pkgs.zip + agda-tools.agda-with-stdlib # Some papers need to compile Agda + ]; phases = [ "buildPhase" ]; @@ -52,10 +54,6 @@ pkgs.stdenv.mkDerivation { cp *.pdf $out ''; - preBuild = lib.optionalString (agdaFile != null) '' - agda-with-stdlib --latex ${agdaFile} --latex-dir . - ''; - meta = with lib; { inherit description; license = licenses.asl20; diff --git a/nix/latex-documents.nix b/nix/latex-documents.nix index 9d6d7a55f45..eef8cedf97e 100644 --- a/nix/latex-documents.nix +++ b/nix/latex-documents.nix @@ -54,6 +54,12 @@ src = self + /doc/plutus-report; }; + utxoma-paper = build-latex-doc { + name = "utxoma-paper"; + description = "utxoma"; + src = self + /doc/papers/utxoma; + }; + system-f-in-agda-paper = build-latex-doc { name = "system-f-in-agda-paper"; description = "system-f in agda"; @@ -61,12 +67,6 @@ agdaFile = "paper.lagda"; }; - utxoma-paper = build-latex-doc { - name = "utxoma-paper"; - description = "utxoma"; - src = self + /doc/papers/utxoma; - }; - unraveling-recursion-paper = build-latex-doc { name = "unraveling-recursion-paper"; description = "unraveling recursion-paper"; From d0a3bf373e4458f887457e346fbf4cb37ffd0c23 Mon Sep 17 00:00:00 2001 From: zeme Date: Thu, 24 Apr 2025 14:53:16 +0200 Subject: [PATCH 3/5] wip --- nix/outputs.nix | 1 - 1 file changed, 1 deletion(-) diff --git a/nix/outputs.nix b/nix/outputs.nix index 14996afa6bf..2897a5bfb00 100644 --- a/nix/outputs.nix +++ b/nix/outputs.nix @@ -132,7 +132,6 @@ let inherit agda-tools; inherit r-with-packages; inherit build-latex-doc; - inherit build-latex; inherit extra-artifacts; inherit static-haskell-packages; inherit exposed-haskell-packages; From 278da2021ef298a4cc97b9a93dd2038790f265c4 Mon Sep 17 00:00:00 2001 From: zeme Date: Thu, 24 Apr 2025 15:28:45 +0200 Subject: [PATCH 4/5] wip --- .gitignore | 1 - doc/notes/multi-currency/Makefile | 2 +- .../{main.tex => multi-currency.tex} | 0 nix/latex-documents.nix | 1 + test-latex.sh | 29 +++++++++++++++++++ 5 files changed, 31 insertions(+), 2 deletions(-) rename doc/notes/multi-currency/{main.tex => multi-currency.tex} (100%) create mode 100644 test-latex.sh diff --git a/.gitignore b/.gitignore index f1a61d3704a..3b71565e775 100644 --- a/.gitignore +++ b/.gitignore @@ -114,5 +114,4 @@ plutus-pab/test-node/alonzo-purple/db *.stacks .nvimrc release-* -.worktrees TestCert.* diff --git a/doc/notes/multi-currency/Makefile b/doc/notes/multi-currency/Makefile index db4ba5b7c6a..5e3045043c8 100644 --- a/doc/notes/multi-currency/Makefile +++ b/doc/notes/multi-currency/Makefile @@ -1,5 +1,5 @@ all: - latexmk -pdf main.tex + latexmk -pdf multi-currency.tex clean: latexmk -C && rm -f *.bbl *.nlo *.nls *.ist *.thm diff --git a/doc/notes/multi-currency/main.tex b/doc/notes/multi-currency/multi-currency.tex similarity index 100% rename from doc/notes/multi-currency/main.tex rename to doc/notes/multi-currency/multi-currency.tex diff --git a/nix/latex-documents.nix b/nix/latex-documents.nix index eef8cedf97e..a4bf24aaf03 100644 --- a/nix/latex-documents.nix +++ b/nix/latex-documents.nix @@ -74,3 +74,4 @@ agdaFile = "paper.lagda"; }; } + diff --git a/test-latex.sh b/test-latex.sh new file mode 100644 index 00000000000..9b9e4b85ccc --- /dev/null +++ b/test-latex.sh @@ -0,0 +1,29 @@ +TARGETS=( + "cost-model-notes cost-model-notes.pdf doc/notes/cost-model-notes" + "eutxo-paper eutxo.pdf doc/papers/eutxo" + "eutxoma-paper eutxoma.pdf doc/papers/eutxoma" + "extended-utxo-spec extended-utxo-specification.pdf doc/extended-utxo-spec" + "lazy-machine-notes lazy-plutus-core.pdf doc/notes/fomega/lazy-machine" + "multi-currency-notes multi-currency.pdf doc/notes/multi-currency" + "plutus-core-spec-old plutus-core-specification.pdf doc/plutus-core-spec-old" + "plutus-core-spec plutus-core-specification.pdf doc/plutus-core-spec" + "plutus-report plutus.pdf doc/plutus-report" + "utxoma-paper utxoma.pdf doc/papers/utxoma" + "system-f-in-agda-paper system-f-in-agda.pdf doc/papers/system-f-in-agda" + "unraveling-recursion-paper unraveling-recursion.pdf doc/papers/unraveling-recursion" +) + +OUTDIR=$(realpath test-latex) +mkdir $OUTDIR +rm $OUTDIR/*.pdf + +for TARGET in "${TARGETS[@]}"; do + IFS=' ' read -r NIX_NAME PDF_NAME FOLDER <<< "$TARGET" + pushd $FOLDER + make clean + make + cp $PDF_NAME "$OUTDIR/$NIX_NAME-shell.pdf" + nix build .#$NIX_NAME + cp result/$PDF_NAME.pdf $OUTDIR/$NIX_NAME-nix.pdf + popd +done \ No newline at end of file From 72e4199208a868ed80336f3cbbd8600465364ef3 Mon Sep 17 00:00:00 2001 From: zeme Date: Thu, 24 Apr 2025 16:30:55 +0200 Subject: [PATCH 5/5] wip --- nix/build-latex-doc.nix | 32 ++++++-------------------------- nix/latex-documents.nix | 2 -- test-latex.sh | 29 ----------------------------- 3 files changed, 6 insertions(+), 57 deletions(-) delete mode 100644 test-latex.sh diff --git a/nix/build-latex-doc.nix b/nix/build-latex-doc.nix index 55c3be2a9cb..e4b9c07b47d 100644 --- a/nix/build-latex-doc.nix +++ b/nix/build-latex-doc.nix @@ -1,26 +1,7 @@ -{ pkgs, lib }: +{ pkgs, lib, agda-tools }: { name, description, src }: -let - - latexEnvironment = pkgs.texliveFull; - # pkgs.texlive.combine { - # inherit (pkgs.texlive) - # acmart - # bibtex - # biblatex - # collection-bibtexextra - # collection-fontsextr - # collection-fontsrecommended - # collection-latex - # collection-latexextr - # collection-luatex - # collection-mathscience scheme-small - # latexmk; - # }; -in - pkgs.stdenv.mkDerivation { inherit name; @@ -36,22 +17,21 @@ pkgs.stdenv.mkDerivation { ".agda" ".agda-lib" ".lagda" - ".md" ".latexmkrc" "Makefile" ]; buildInputs = [ - latexEnvironment + pkgs.texliveFull pkgs.zip agda-tools.agda-with-stdlib # Some papers need to compile Agda ]; - phases = [ "buildPhase" ]; - - buildPhase = '' + installPhase = '' + mkdir -p $out + make clean make - cp *.pdf $out + cp *.pdf $out/ ''; meta = with lib; { diff --git a/nix/latex-documents.nix b/nix/latex-documents.nix index a4bf24aaf03..0240d59db5b 100644 --- a/nix/latex-documents.nix +++ b/nix/latex-documents.nix @@ -64,14 +64,12 @@ name = "system-f-in-agda-paper"; description = "system-f in agda"; src = self + /doc/papers/system-f-in-agda; - agdaFile = "paper.lagda"; }; unraveling-recursion-paper = build-latex-doc { name = "unraveling-recursion-paper"; description = "unraveling recursion-paper"; src = self + /doc/papers/unraveling-recursion; - agdaFile = "paper.lagda"; }; } diff --git a/test-latex.sh b/test-latex.sh deleted file mode 100644 index 9b9e4b85ccc..00000000000 --- a/test-latex.sh +++ /dev/null @@ -1,29 +0,0 @@ -TARGETS=( - "cost-model-notes cost-model-notes.pdf doc/notes/cost-model-notes" - "eutxo-paper eutxo.pdf doc/papers/eutxo" - "eutxoma-paper eutxoma.pdf doc/papers/eutxoma" - "extended-utxo-spec extended-utxo-specification.pdf doc/extended-utxo-spec" - "lazy-machine-notes lazy-plutus-core.pdf doc/notes/fomega/lazy-machine" - "multi-currency-notes multi-currency.pdf doc/notes/multi-currency" - "plutus-core-spec-old plutus-core-specification.pdf doc/plutus-core-spec-old" - "plutus-core-spec plutus-core-specification.pdf doc/plutus-core-spec" - "plutus-report plutus.pdf doc/plutus-report" - "utxoma-paper utxoma.pdf doc/papers/utxoma" - "system-f-in-agda-paper system-f-in-agda.pdf doc/papers/system-f-in-agda" - "unraveling-recursion-paper unraveling-recursion.pdf doc/papers/unraveling-recursion" -) - -OUTDIR=$(realpath test-latex) -mkdir $OUTDIR -rm $OUTDIR/*.pdf - -for TARGET in "${TARGETS[@]}"; do - IFS=' ' read -r NIX_NAME PDF_NAME FOLDER <<< "$TARGET" - pushd $FOLDER - make clean - make - cp $PDF_NAME "$OUTDIR/$NIX_NAME-shell.pdf" - nix build .#$NIX_NAME - cp result/$PDF_NAME.pdf $OUTDIR/$NIX_NAME-nix.pdf - popd -done \ No newline at end of file