lambda_mountain 1.16.40

Typed Macro Assembler (backed by Coq proofs-of-correctness)
Documentation 
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
68
69
70


work: compile-production
	./production tests/regress/mono-struct.lm
	as tmp.s -o tmp.o
	ld tmp.o -o tmp
	./tmp

build-docs:
	lm --blob -o docs/index.html docs/index.html.lm
	doby doc -o docs/default.html.html.lm LIB/default.html
	doby doc -o docs/default.lm.html.lm LIB/default.lm
	doby doc -o docs/lm.lm.html.lm SRC/cli.lm
	lm --blob -o docs/default.html.html docs/default.html.html.lm
	lm --blob -o docs/default.lm.html docs/default.lm.html.lm
	lm --blob -o docs/lm.lm.html docs/lm.lm.html.lm

develop:
	lmv tests/regress/hello_world.s.v
	coqc tmp.v
	coqchk tmp.vo

deploy: compile-production build-docs
	time ./production -o deploy.s SRC/cli.lm
	as deploy.s -o deploy.o
	ld deploy.o -o deploy
	time ./deploy -o deploy2.s SRC/cli.lm
	diff deploy.s deploy2.s
	mv deploy.s BOOTSTRAP/cli.s
	cargo test regression_tests

compile-dev: compile-bootstrap
	rm -f dev dev.o dev.s
	./bootstrap -o dev.s DEV/cli.lm
	as -o dev.o dev.s
	ld -o dev   dev.o

compile-production: compile-bootstrap
	rm -f production production.o production.s
	./bootstrap -o production.s SRC/cli.lm
	as -o production.o production.s
	ld -o production   production.o
	cp production re-production

compile-bootstrap:
	rm -f bootstrap bootstrap.o
	as -o bootstrap.o BOOTSTRAP/cli.s
	ld -o bootstrap   bootstrap.o

install:
	as -o lm_raw.o BOOTSTRAP/cli.s
	ld -o lm lm_raw.o
	mv lm /usr/local/bin/
	rm lm_raw.o
	#lm LMV/cli.lm -o lmv.s
	#as -o lmv.o lmv.s
	#ld -o lmv   lmv.o
	#mv lmv /usr/local/bin
	#rm lmv.s lmv.o
	lm DOBY/cli.lm -o doby.s
	as -o doby.o doby.s
	ld -o doby   doby.o
	mv doby /usr/local/bin
	rm doby.s doby.o

validate:
	coqc LIB/default_validator.v
	coqchk LIB/default_validator.vo

disassemble:
	objdump -S hello_world