blob: 8f5fdb1848c343a9a462c88f917c64342984c4cb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
all: test lib
DEPLOY_DEST ?= vps:/var/www/naproche.org/
RSYNC_FLAGS ?= -az --delete-delay --itemize-changes --exclude=".DS_Store"
TYPED_LIBRARY_ROOT := library/everything.tex
# The active aggregate covers the complete production library graph.
.PHONY: lib
lib:
stack build
@set -e; \
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
.PHONY: dump
dump:
stack build
@dump_dir="$(DUMP_DIR)"; \
if test -z "$$dump_dir"; then \
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"
.PHONY: build
build:
stack build
.PHONY: test golden
test:
stack test
golden:
stack test --test-arguments "--accept"
.PHONY: publish
publish:
rsync $(RSYNC_FLAGS) html/ $(DEPLOY_DEST)
.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
.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
.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
|
