From 97ac9b6b0e06c7ac9ea6d2361d86aac830241e1b Mon Sep 17 00:00:00 2001 From: davidcok Date: Fri, 29 Jan 2021 12:41:35 -0500 Subject: [PATCH 01/35] Adding quicktest --- .github/workflows/release-downloads.yml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/workflows/release-downloads.yml b/.github/workflows/release-downloads.yml index 368ba404ee2..dc778eb4c4b 100644 --- a/.github/workflows/release-downloads.yml +++ b/.github/workflows/release-downloads.yml @@ -84,6 +84,10 @@ jobs: if: runner.os == 'Windows' run: (dafny/Dafny.exe /compile:0 b.dfy || echo "EXPECTED FAILURE") ; exit 0 ## Check that a simple program compiles and runs on each supported platform + - name: run quicktests + run: | + dafny/quicktest.sh > log.txt + diff log.txt dafny/quicktest.out - name: Check C# compile run: | dafny/dafny /compileVerbose:0 /compile:3 /compileTarget:cs /spillTargetCode:3 a.dfy From 87f0eee292ba37053aabb71cc32cbccee622bb92 Mon Sep 17 00:00:00 2001 From: davidcok Date: Thu, 14 Jul 2022 08:11:36 -0400 Subject: [PATCH 02/35] Edit per comment from Remy --- docs/DafnyRef/Introduction.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/DafnyRef/Introduction.md b/docs/DafnyRef/Introduction.md index 823f29ad02f..4ec609364cd 100644 --- a/docs/DafnyRef/Introduction.md +++ b/docs/DafnyRef/Introduction.md @@ -29,8 +29,8 @@ changing the program’s type declarations, specifications, and statements. and `dafny` to refer to the software tool that verifies and compiles programs in the Dafny language.) -The easiest way to try out `dafny` is to [download](https://github.com/dafny-lang/dafny/releases) it -to run it on your machine as you follow along with the [Dafny tutorial](../OnlineTutorial/guide). +The easiest way to try out the Dafny language is to [download the supporting tools and documentation](https://github.com/dafny-lang/dafny/releases) and +run `dafny` on your machine as you follow along with the [Dafny tutorial](../OnlineTutorial/guide). The `dafny` tool can be run from the command line (on Linux, MacOS, Windows or other platforms) or from an IDE such as emacs or an editor such as VSCode, which can provide syntax highlighting without the built-in verification. From 47815c1a3e7c0a66140d3b7960aac120b007abe8 Mon Sep 17 00:00:00 2001 From: davidcok Date: Wed, 21 Sep 2022 09:11:09 -0400 Subject: [PATCH 03/35] Checking included files --- docs/_includes/custom-head.html | 2 ++ docs/_includes/footer.html | 1 + docs/_includes/head.html | 1 + docs/_includes/header.html | 1 + docs/_layouts/default.html | 1 + 5 files changed, 6 insertions(+) diff --git a/docs/_includes/custom-head.html b/docs/_includes/custom-head.html index 8559a67ffad..d5113b87220 100644 --- a/docs/_includes/custom-head.html +++ b/docs/_includes/custom-head.html @@ -4,3 +4,5 @@ 1. Head over to https://realfavicongenerator.net/ to add your own favicons. 2. Customize default _includes/custom-head.html in your source directory and insert the given code snippet. {% endcomment %} + +CUSTOM diff --git a/docs/_includes/footer.html b/docs/_includes/footer.html index 03e4d2d11d9..a280d5a1fd2 100644 --- a/docs/_includes/footer.html +++ b/docs/_includes/footer.html @@ -1,4 +1,5 @@