Install dafny lang binaries and run inside a terminal, no vscode or emacs needed.

Makefile

#
# 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)