search

project-everest / vale

Verified Assembly Language for Everest
Apache License 2.0
270 stars 20 forks source link

Any plan to release Vale with the latest Dafny? #42

Open superymk opened 4 years ago

superymk commented 4 years ago

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 commented 4 years ago

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_dafnydirect.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.