diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 59 |
1 files changed, 43 insertions, 16 deletions
@@ -5,6 +5,27 @@ RSYNC_FLAGS ?= -az --delete-delay --itemize-changes --exclude=".DS_Store" TYPED_LIBRARY_ROOT := library/everything.tex +PARITY_ROOTS := \ + test/examples/abbr.tex \ + test/examples/byRef.tex \ + test/examples/calc.tex \ + test/examples/coord.tex \ + test/examples/datatype.tex \ + test/examples/finite-set-terms.tex \ + test/examples/formula.tex \ + test/examples/indefinite-terms.tex \ + test/examples/inductive.tex \ + test/examples/no-reflexive-set.tex \ + test/examples/proofassume.tex \ + test/examples/proofdefinefunction.tex \ + test/examples/prooffix.tex \ + test/examples/relation-notation.tex \ + test/examples/relparam.tex \ + test/examples/replace.tex \ + test/examples/russell.tex \ + test/examples/separation.tex \ + test/examples/union.tex + # The active aggregate covers the complete production library graph. .PHONY: lib lib: @@ -13,8 +34,20 @@ lib: store_dir="$$(mktemp -d "$${TMPDIR:-/tmp}/felix-lib.XXXXXX")"; \ trap 'rm -rf "$$store_dir"' EXIT; \ printf 'Verifying %s\n' "$(TYPED_LIBRARY_ROOT)"; \ - time stack exec zf -- --store "$$store_dir/store.sqlite" \ - --log "$(TYPED_LIBRARY_ROOT)" -t 20 + time stack exec felix -- --store "$$store_dir/store.sqlite" \ + "$(TYPED_LIBRARY_ROOT)" -t 20 + +.PHONY: parity +parity: + stack build + @set -e; \ + store_dir="$$(mktemp -d "$${TMPDIR:-/tmp}/felix-parity.XXXXXX")"; \ + trap 'rm -rf "$$store_dir"' EXIT; \ + for root in $(PARITY_ROOTS); do \ + printf 'Verifying parity root %s\n' "$$root"; \ + stack exec felix -- --store "$$store_dir/store.sqlite" \ + "$$root" -t 20; \ + done .PHONY: dump dump: @@ -24,7 +57,7 @@ dump: dump_dir="$$(mktemp -d "$${TMPDIR:-/tmp}/felix-dump.XXXXXX")"; \ fi; \ printf 'Writing dump to %s\n' "$$dump_dir"; \ - time stack exec zf -- --fresh --log library/everything.tex -t 17 --dump "$$dump_dir" + time stack exec felix -- --fresh library/everything.tex -t 17 --dump "$$dump_dir" .PHONY: build build: @@ -44,24 +77,18 @@ publish: .PHONY: profile profile: stack --work-dir .stack-work-profile build --profile --ghc-options "-fprof-auto -fprof-cafs" - stack --work-dir .stack-work-profile exec --profile zf -- debug/formalizations_with_section_20_up_to_euclidean_metric_theorem.tex +RTS -s -p - ghc-prof-flamegraph zf.prof - -.PHONY: profilenominal -profilenominal: - stack --work-dir .stack-work-profile build --profile --ghc-options "-fprof-auto -fprof-cafs" - stack --work-dir .stack-work-profile exec --profile zf -- debug/formalizations_with_section_20_up_to_euclidean_metric_theorem.tex --nominal +RTS -s -p - ghc-prof-flamegraph zf.prof + stack --work-dir .stack-work-profile exec --profile felix -- --fresh -t 20 library/everything.tex +RTS -s -p + ghc-prof-flamegraph felix.prof .PHONY: profilemem profilemem: stack --work-dir .stack-work-profile build --profile --ghc-options "-fprof-auto -fprof-cafs" - stack --work-dir .stack-work-profile exec --profile zf -- debug/formalizations_with_section_20_up_to_euclidean_metric_theorem.tex +RTS -hc -RTS - hp2ps zf.hp - gs -q -dNOPAUSE -dBATCH -sOutputFile=temp.ps -sDEVICE=ps2write -c "<</Orientation 1>> setpagedevice" -- zf.ps && mv temp.ps zf.ps + stack --work-dir .stack-work-profile exec --profile felix -- --fresh -t 20 library/everything.tex +RTS -hc -RTS + hp2ps felix.hp + gs -q -dNOPAUSE -dBATCH -sOutputFile=temp.ps -sDEVICE=ps2write -c "<</Orientation 1>> setpagedevice" -- felix.ps && mv temp.ps felix.ps .PHONY: profileparser profileparser: stack --work-dir .stack-work-profile build --profile --ghc-options "-fprof-auto -fprof-cafs" - stack --work-dir .stack-work-profile exec --profile zf -- debug/formalizations_with_section_20_up_to_euclidean_metric_theorem.tex --parseonly +RTS -p - ghc-prof-flamegraph zf.prof + stack --work-dir .stack-work-profile exec --profile felix -- --fresh -t 20 library/everything.tex --parseonly +RTS -p + ghc-prof-flamegraph felix.prof |