forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Makefile
103 lines (80 loc) · 4.16 KB
/
Makefile
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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
DIR=$(realpath $(dir $(firstword $(MAKEFILE_LIST))))
default: exe
all: exe refman
exe:
(cd ${DIR} ; dotnet build Source/Dafny.sln ) ## includes parser
format-dfy:
(cd "${DIR}"/Source/DafnyCore ; ../../Binaries/Dafny.exe format .)
dfy-to-cs:
(cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh)
dfy-to-cs-exe: dfy-to-cs
(cd ${DIR} ; dotnet build Source/Dafny.sln )
dfy-to-cs-noverify:
(cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh --no-verify)
dfy-to-cs-noverify-exe: dfy-to-cs-noverify exe
boogie: ${DIR}/boogie/Binaries/Boogie.exe
tests:
(cd ${DIR}; dotnet test Source/IntegrationTests)
tests-verbose:
(cd ${DIR}; dotnet test --logger "console;verbosity=normal" Source/IntegrationTests )
${DIR}/boogie/Binaries/Boogie.exe:
(cd ${DIR}/boogie ; dotnet build -c Release Source/Boogie.sln )
refman: exe
make -C ${DIR}/docs/DafnyRef
refman-release: exe
make -C ${DIR}/docs/DafnyRef release
z3-mac:
mkdir -p ${DIR}/Binaries/z3/bin
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-macos-11-bin.zip
unzip z3-4.12.1-x64-macos-11-bin.zip
rm z3-4.12.1-x64-macos-11-bin.zip
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip
unzip z3-4.8.5-x64-macos-11-bin.zip
rm z3-4.8.5-x64-macos-11-bin.zip
mv z3-* ${DIR}/Binaries/z3/bin/
chmod +x ${DIR}/Binaries/z3/bin/z3-*
z3-mac-arm:
mkdir -p ${DIR}/Binaries/z3/bin
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-arm64-macos-11-bin.zip
unzip z3-4.12.1-arm64-macos-11-bin.zip
rm z3-4.12.1-arm64-macos-11-bin.zip
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-macos-11-bin.zip
unzip z3-4.8.5-x64-macos-11-bin.zip
rm z3-4.8.5-x64-macos-11-bin.zip
mv z3-* ${DIR}/Binaries/z3/bin/
chmod +x ${DIR}/Binaries/z3/bin/z3-*
z3-ubuntu:
mkdir -p ${DIR}/Binaries/z3/bin
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip
unzip z3-4.12.1-x64-ubuntu-20.04-bin.zip
rm z3-4.12.1-x64-ubuntu-20.04-bin.zip
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.8.5-x64-ubuntu-20.04-bin.zip
unzip z3-4.8.5-x64-ubuntu-20.04-bin.zip
rm z3-4.8.5-x64-ubuntu-20.04-bin.zip
mv z3-* ${DIR}/Binaries/z3/bin/
chmod +x ${DIR}/Binaries/z3/bin/z3-*
format:
dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny/* --exclude Source/DafnyCore.Test/GeneratedFromDafny/* --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
clean:
(cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
(cd ${DIR} ; dotnet build Source/Dafny.sln -v:q --nologo -target:clean )
make -C ${DIR}/Source/DafnyCore -f Makefile clean
(cd ${DIR}/Source/Dafny && rm -rf Scanner.cs Parser.cs obj )
(cd ${DIR}/Source/DafnyRuntime/DafnyRuntimeJava; ./gradlew clean)
make -C ${DIR}/docs/DafnyRef clean
(cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
echo Source/*/bin Source/*/obj
update-cs-module:
(cd ${DIR}; cd Source/DafnyRuntime; make update-system-module)
update-go-module:
(cd ${DIR}; cd Source/DafnyRuntime/DafnyRuntimeGo; make update-system-module)
update-runtime-dafny:
(cd ${DIR}; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go)
# `make pr` will bring you in a state suitable for submitting a PR
# - Builds the Dafny executable
# - Use the build to convert core .dfy files to .cs
# - Rebuilds the Dafny executable with this .cs files
# - Apply dafny format on all dfy files
# - Apply dotnet format on all cs files except the generated ones
# - Rebuild the Go and C# runtime modules as needed.
pr: exe dfy-to-cs-exe format-dfy format update-runtime-dafny update-cs-module update-go-module