Last active
November 10, 2023 04:14
-
-
Save lcharles123/dc33f095a39dee6f15d3ad2ec68f304a to your computer and use it in GitHub Desktop.
Install dafny lang binaries and run inside a terminal, no vscode or emacs needed.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
# | |
# Use Dafny lang in any system: setup agnostic | |
# Tested on Ubuntu 18.04 | |
# install java | |
# apt install default-jre | |
# | |
# install dotnet 6.0 from Microsoft site | |
# https://dotnet.microsoft.com/en-us/download/dotnet/6.0 | |
# | |
# install these programs from source: | |
# follow the instructions in the respective README | |
# git clone https://github.com/dafny-lang/dafny | |
# git checkout 4.3.0 # or the next one | |
# | |
# git clone https://github.com/Z3Prover/z3 | |
# git checkout 4.12.2 # or the next one | |
# FIXME LOCATE AND SET PARAMETERS: | |
NET_RUNTIME=dotnet | |
DAFNY=/root/dafny/Binaries/Dafny.dll | |
# can use DafnyDriver.dll too | |
INPUT=test.dfy | |
args= | |
# List of Comands (Targets): | |
# resolve <file> Only check for parse and type resolution errors. | |
# verify <file> Verify the program. | |
# build <file> Produce an executable binary or a library. | |
# run <file> <program-arguments> Run the program. [] | |
# translate Translate Dafny sources to source and build files in a specified language. | |
# audit <file> Report issues in the Dafny code that might limit the soundness claims of verification, emitting them as warnings or in a report document. | |
run: | |
$(NET_RUNTIME) $(DAFNY) $@ $(INPUT) $(args) | |
#Dafny run <file> [<program-arguments>...] [options] | |
#Options: | |
# --enforce-determinism Check that only deterministic statements are used, so that values seen during execution will be the same in every run of the program. | |
# --test-assumptions <Externs|None> (experimental) When turned on, inserts runtime tests at locations where (implicit) assumptions occur, such as when calling or being called by external code and when using assume statements. | |
# --verification-time-limit <seconds> Limit the number of seconds spent trying to verify each procedure | |
# --manual-lemma-induction Turn off automatic induction for lemmas. | |
# --solver-path <solver-path> Can be used to specify a custom SMT solver to use for verifying Dafny proofs. | |
# --isolate-assertions Verify each assertion in isolation. | |
# --boogie <arguments> Specify arguments that are passed to Boogie, a tool used to verify Dafny programs. | |
# --log-format <configuration> Logs verification results using the given test result format. The currently supported formats are `trx`, `csv`, and `text`. These are: the XML-based format commonly used for test results for .NET languages, a custom CSV schema, and a textual format meant for human consumption. You can provide configuration using the same string format as when using the --logger option for dotnet test, such as: --format "trx;LogFileName=<...>"); | |
# --resource-limit <resource-limit> Specify the maximum resource limit (rlimit) value to pass to Z3. A resource limit is a deterministic alternative to a time limit. The output produced by `--log-format csv` includes the resource use of each proof effort, which you can use to determine an appropriate limit for your program. Multiplied by 1000 before sending to Z3. | |
# --solver-plugin <solver-plugin> Dafny uses Boogie as part of its verification process. This option allows customising that part using a Boogie plugin. More information about Boogie can be found at https://github.com/boogie-org/boogie. Information on how to construct Boogie plugins can be found by looking at the code in https://github.com/boogie-org/boogie/blob/v2.16.3/Source/Provers/SMTLib/ProverUtil.cs#L316 | |
# --error-limit <error-limit> Set the maximum number of errors to report (0 for unlimited). [default: 5] | |
# --show-snippets Show a source code snippet for each Dafny message. [default: True] | |
# --warn-as-errors Treat warnings as errors. | |
# --warn-shadowing Emits a warning if the name of a declared variable caused another variable to be shadowed. | |
# --warn-missing-constructor-parentheses Emits a warning when a constructor name in a case pattern is not followed by parentheses. | |
# --track-print-effects A compiled method, constructor, or iterator is allowed to have print effects only if it is marked with {{:print}}. | |
# --stdin Read standard input and treat it as an input .dfy file. [default: False] | |
# --verbose Print additional information such as which files are emitted where. | |
# --cores <count> Run the Dafny verifier using <n> cores, or using <XX%> of the machine's logical cores. [default: 2] | |
# --library <library> The contents of this file and any files it includes can be referenced from other files as if they were included. | |
# --prelude <file> Choose the Dafny prelude file. | |
# --function-syntax <version> The syntax for functions changed from Dafny version 3 to version 4. This switch controls access to the new syntax, and also provides a mode to help with migration. | |
# --use-basename-for-filename When parsing use basename of file for tokens instead of the path supplied on the command line | |
# --reads-clauses-on-methods Allows reads clauses on methods (with a default of 'reads *') as well as functions. | |
# --standard-libraries Allow Dafny code to depend on the standard libraries included with the Dafny distribution. | |
r: resolve | |
resolve: | |
$(NET_RUNTIME) $(DAFNY) $@ $(INPUT) $(args) | |
v: verify | |
verify: | |
$(NET_RUNTIME) $(DAFNY) $@ $(INPUT) $(args) | |
b: build | |
build: | |
$(NET_RUNTIME) $(DAFNY) $@ $(INPUT) $(args) | |
t: translate | |
translate: | |
$(NET_RUNTIME) $(DAFNY) $@ $(INPUT) $(args) | |
a: audit | |
audit: | |
$(NET_RUNTIME) $(DAFNY) $@ $(INPUT) $(args) | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment