Any plan to release Vale with the latest Dafny?

[superymk]

Latest Dafny changes syntax a little bit. For example, Dafny-v1.9.9 complains "!new" which is needed in Dafny-v2.3 in my project.
I also tried to build Vale with the latest Dafny (v2.3.0), but got compilation errors. I'll post my setup and the errors later. Thanks!

[superymk]

Here is my setup to build the latest Vale:

(1) Ubuntu 18.04.3 LTS x64, with Python 3.6.8
(2) sudo apt install scons fsharp nuget mono-devel
(3) Vale-0.3.10 source code (https://github.com/project-everest/vale/archive/v0.3.10.zip), Dafny-2.3.0 binary (https://github.com/dafny-lang/dafny/releases/download/v2.3.0/dafny-2.3.0.10506-x64-ubuntu-16.04.zip). I put Vale in ~/utils/vale, and Dafny in ~/utils/dafny
(4) Build Vale with "scons --DAFNY-PATH=../dafny"

Error output:
scons: Reading SConscript files ...
Processing source files
scons: done reading SConscript files.
scons: Building targets ...
Copy file(s): "/home/superymk/utils/dafny/BoogieAbsInt.dll" to "bin/BoogieAbsInt.dll"
Copy file(s): "/home/superymk/utils/dafny/BoogieBasetypes.dll" to "bin/BoogieBasetypes.dll"
Copy file(s): "/home/superymk/utils/dafny/BoogieCodeContractsExtender.dll" to "bin/BoogieCodeContractsExtender.dll"
Copy file(s): "/home/superymk/utils/dafny/BoogieConcurrency.dll" to "bin/BoogieConcurrency.dll"
Copy file(s): "/home/superymk/utils/dafny/BoogieCore.dll" to "bin/BoogieCore.dll"
Copy file(s): "/home/superymk/utils/dafny/BoogieDoomed.dll" to "bin/BoogieDoomed.dll"
Copy file(s): "/home/superymk/utils/dafny/BoogieExecutionEngine.dll" to "bin/BoogieExecutionEngine.dll"
Copy file(s): "/home/superymk/utils/dafny/BoogieGraph.dll" to "bin/BoogieGraph.dll"
Copy file(s): "/home/superymk/utils/dafny/BoogieHoudini.dll" to "bin/BoogieHoudini.dll"
Copy file(s): "/home/superymk/utils/dafny/BoogieModel.dll" to "bin/BoogieModel.dll"
Copy file(s): "/home/superymk/utils/dafny/BoogieParserHelper.dll" to "bin/BoogieParserHelper.dll"
Copy file(s): "/home/superymk/utils/dafny/BoogieVCExpr.dll" to "bin/BoogieVCExpr.dll"
Copy file(s): "/home/superymk/utils/dafny/BoogieVCGeneration.dll" to "bin/BoogieVCGeneration.dll"
Copy file(s): "/home/superymk/utils/dafny/Dafny.exe" to "bin/Dafny.exe"
dmcs -t:library -out:/home/superymk/utils/vale/bin/DafnyInterface.dll /home/superymk/utils/vale/tools/Vale/DafnyInterface/Source/DafnyInterface/DafnyDriver.cs /home/superymk/utils/vale/tools/Vale/DafnyInterface/Source/DafnyInterface/Properties/AssemblyInfo.cs -r:/home/superymk/utils/dafny/BoogieAbsInt.dll -r:/home/superymk/utils/dafny/BoogieConcurrency.dll -r:/home/superymk/utils/dafny/BoogieCore.dll -r:/home/superymk/utils/dafny/BoogieExecutionEngine.dll -r:/home/superymk/utils/dafny/BoogieParserHelper.dll -r:/home/superymk/utils/dafny/BoogieVCGeneration.dll -r:/home/superymk/utils/dafny/Dafny.exe -r:/home/superymk/utils/dafny/DafnyPipeline.dll -r:/home/superymk/utils/dafny/Provers.SMTLib.dll
Note: dmcs is deprecated, please use mcs instead!
warning CS8001: SDK path could not be resolved
Compilation succeeded - 1 warning(s)
Copy file(s): "/home/superymk/utils/dafny/DafnyPipeline.dll" to "bin/DafnyPipeline.dll"
Copy file(s): "/home/superymk/utils/dafny/DafnyPrelude.bpl" to "bin/DafnyPrelude.bpl"
Copy file(s): "/home/superymk/utils/dafny/DafnyRuntime.cs" to "bin/DafnyRuntime.cs"
Copy file(s): "/home/superymk/utils/dafny/Provers.SMTLib.dll" to "bin/Provers.SMTLib.dll"
fsharpc -g --platform:anycpu --standalone --mlcompatibility -O /home/superymk/utils/vale/tools/Vale/src/ast.fs /home/superymk/utils/vale/tools/Vale/src/ast_util.fs /home/superymk/utils/vale/tools/Vale/src/parse_util.fs /home/superymk/utils/vale/obj/Vale/parse.fs /home/superymk/utils/vale/obj/Vale/lex.fs /home/superymk/utils/vale/tools/Vale/src/emit_vale_text.fs /home/superymk/utils/vale/tools/Vale/src/typechecker.fs /home/superymk/utils/vale/tools/Vale/src/transform.fs /home/superymk/utils/vale/tools/Vale/src/emit_common_base.fs /home/superymk/utils/vale/tools/Vale/src/emit_common_quick_code.fs /home/superymk/utils/vale/tools/Vale/src/emit_common_lemmas.fs /home/superymk/utils/vale/tools/Vale/src/emit_common_quick_export.fs /home/superymk/utils/vale/tools/Vale/src/emit_common_top.fs /home/superymk/utils/vale/tools/Vale/src/emit_dafny_text.fs /home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs /home/superymk/utils/vale/tools/Vale/src/emit_fstar_text.fs /home/superymk/utils/vale/tools/Vale/src/main.fs -o /home/superymk/utils/vale/bin/vale.exe -r /home/superymk/utils/dafny/BoogieAbsInt.dll -r /home/superymk/utils/dafny/BoogieBasetypes.dll -r /home/superymk/utils/dafny/BoogieCodeContractsExtender.dll -r /home/superymk/utils/dafny/BoogieConcurrency.dll -r /home/superymk/utils/dafny/BoogieCore.dll -r /home/superymk/utils/dafny/BoogieDoomed.dll -r /home/superymk/utils/dafny/BoogieExecutionEngine.dll -r /home/superymk/utils/dafny/BoogieGraph.dll -r /home/superymk/utils/dafny/BoogieHoudini.dll -r /home/superymk/utils/dafny/BoogieModel.dll -r /home/superymk/utils/dafny/BoogieParserHelper.dll -r /home/superymk/utils/dafny/BoogieVCExpr.dll -r /home/superymk/utils/dafny/BoogieVCGeneration.dll -r /home/superymk/utils/dafny/DafnyPipeline.dll -r /home/superymk/utils/dafny/Dafny.exe -r /home/superymk/utils/vale/bin/DafnyInterface.dll -r /home/superymk/utils/vale/tools/Dafny/Newtonsoft.Json.dll -r /home/superymk/utils/vale/tools/FsLexYacc/FsLexYacc.Runtime.6.1.0/lib/net40/FsLexYacc.Runtime.dll
F# Compiler for F# 4.0 (Open Source Edition)
Freely distributed under the Apache 2.0 Open Source License

/home/superymk/utils/vale/tools/Vale/src/emit_common_lemmas.fs(531,13): warning FS0058: Possible incorrect indentation: this token is offside of context started at position (530:22). Try indenting this token further or using standard formatting conventions.

/home/superymk/utils/vale/tools/Vale/src/emit_common_lemmas.fs(531,13): warning FS0058: Possible incorrect indentation: this token is offside of context started at position (530:22). Try indenting this token further or using standard formatting conventions.

/home/superymk/utils/vale/tools/Vale/src/emit_common_lemmas.fs(531,19): warning FS0058: Possible incorrect indentation: this token is offside of context started at position (530:22). Try indenting this token further or using standard formatting conventions.

/home/superymk/utils/vale/tools/Vale/src/emit_common_lemmas.fs(532,13): warning FS0058: Possible incorrect indentation: this token is offside of context started at position (530:22). Try indenting this token further or using standard formatting conventions.

/home/superymk/utils/vale/tools/Vale/src/emit_common_lemmas.fs(532,13): warning FS0058: Possible incorrect indentation: this token is offside of context started at position (530:22). Try indenting this token further or using standard formatting conventions.

/home/superymk/utils/vale/tools/Vale/src/emit_common_lemmas.fs(532,20): warning FS0058: Possible incorrect indentation: this token is offside of context started at position (530:22). Try indenting this token further or using standard formatting conventions.

/home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs(83,25): error FS0039: The type 'ObjectType' is not defined

/home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs(377,11): error FS0501: The member or object constructor 'LambdaExpr' takes 5 argument(s) but is here given 6. The required signature is 'LambdaExpr(tok: Boogie.IToken, bvars: System.Collections.Generic.List, requires: Expression, reads: System.Collections.Generic.List, body: Expression) : unit'.

/home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs(381,38): error FS0033: The type 'Microsoft.Dafny.CasePattern<_>' expects 1 type argument(s) but is given 0

/home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs(384,11): error FS0072: Lookup on object of indeterminate type based on information prior to this program point. A type annotation may be needed prior to this program point to constrain the type of the object. This may allow the lookup to be resolved.

/home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs(450,17): error FS0501: The member or object constructor 'AssertStmt' takes 6 argument(s) but is here given 5. The required signature is 'AssertStmt(tok: Boogie.IToken, endTok: Boogie.IToken, expr: Expression, proof: BlockStmt, label: AssertLabel, attrs: Attributes) : unit'.

/home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs(639,7): error FS0001: The type 'MaybeFreeExpression' does not match the type 'Expression'. See also /home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs(639,6)-(639,10).

/home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs(639,20): error FS0001: The type 'MaybeFreeExpression' does not match the type 'Expression'. See also /home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs(639,19)-(639,22).

/home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs(639,7): error FS0193: Type constraint mismatch. The type
ResizeArray
is not compatible with type
System.Collections.Generic.List
The type 'MaybeFreeExpression' does not match the type 'Expression'. See also /home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs(637,4)-(639,90).

/home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs(640,3): error FS0072: Lookup on object of indeterminate type based on information prior to this program point. A type annotation may be needed prior to this program point to constrain the type of the object. This may allow the lookup to be resolved.

/home/superymk/utils/vale/tools/Vale/src/emit_dafny_direct.fs(641,3): error FS0072: Lookup on object of indeterminate type based on information prior to this program point. A type annotation may be needed prior to this program point to constrain the type of the object. This may allow the lookup to be resolved.
scons: *** [bin/vale.exe] Error 1
scons: building terminated because of errors.