dafny on R-Pi

First step in getting help with a build failure is to report what actually happens. Nobody can guess what you mean by ?crashed?.

--
https://www.greenend.org.uk/rjk/

Richard Kettlewell wrote:

xbuild tool is deprecated and will be removed in future updates, use msbuild instead

XBuild Engine Version 14.0 Mono, Version 5.2.0.215 Copyright (C) 2005-2013 Various Mono authors

Build started 20/09/2017 05:51:13. __________________________________________________ Project "/home/incal/dafny-dafny/boogie/Source/Boogie.sln" (default target(s)): Target ValidateSolutionConfiguration: Building solution configuration "Checked|Mixed Platforms". Target Build: Project "/home/incal/dafny-dafny/boogie/Source/CodeContractsExtender/CodeContractsExtender.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/CodeContractsExtender/CodeContractsExtender.csproj". Project "/home/incal/dafny-dafny/boogie/Source/Model/Model.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/Model/Model.csproj". Project "/home/incal/dafny-dafny/boogie/Source/Graph/Graph.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/Graph/Graph.csproj". Project "/home/incal/dafny-dafny/boogie/Source/Basetypes/Basetypes.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/Basetypes/Basetypes.csproj". Project "/home/incal/dafny-dafny/boogie/Source/ParserHelper/ParserHelper.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/ParserHelper/ParserHelper.csproj". Project "/home/incal/dafny-dafny/boogie/Source/ModelViewer/ModelViewer.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: x86 Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/ModelViewer/ModelViewer.csproj". Project "/home/incal/dafny-dafny/boogie/Source/Core/Core.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/Core/Core.csproj". Project "/home/incal/dafny-dafny/boogie/Source/BVD/BVD.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Target _CopyAppConfigFile: Skipping target "_CopyAppConfigFile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/BVD/BVD.csproj". Project "/home/incal/dafny-dafny/boogie/Source/UnitTests/BasetypesTests/BasetypesTests.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/UnitTests/BasetypesTests/BasetypesTests.csproj". Project "/home/incal/dafny-dafny/boogie/Source/AbsInt/AbsInt.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/AbsInt/AbsInt.csproj". Project "/home/incal/dafny-dafny/boogie/Source/VCExpr/VCExpr.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/VCExpr/VCExpr.csproj". Project "/home/incal/dafny-dafny/boogie/Source/Concurrency/Concurrency.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Target _CopyAppConfigFile: Skipping target "_CopyAppConfigFile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/Concurrency/Concurrency.csproj". Project "/home/incal/dafny-dafny/boogie/Source/UnitTests/TestUtil/TestUtil.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/UnitTests/TestUtil/TestUtil.csproj". Project "/home/incal/dafny-dafny/boogie/Source/VCGeneration/VCGeneration.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/VCGeneration/VCGeneration.csproj". Project "/home/incal/dafny-dafny/boogie/Source/UnitTests/CoreTests/CoreTests.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/UnitTests/CoreTests/CoreTests.csproj". Project "/home/incal/dafny-dafny/boogie/Source/Provers/SMTLib/SMTLib.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/Provers/SMTLib/SMTLib.csproj". Project "/home/incal/dafny-dafny/boogie/Source/Predication/Predication.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Skipping target "CoreCompile" because its outputs are up-to-date. Done building project "/home/incal/dafny-dafny/boogie/Source/Predication/Predication.csproj". Project "/home/incal/dafny-dafny/boogie/Source/Doomed/Doomed.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target _GenerateTargetFrameworkMonikerAttribute: Skipping target "_GenerateTargetFrameworkMonikerAttribute" because its outputs are up-to-date. Target CoreCompile: Tool /usr/lib/mono/4.5/csc.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Debug/BoogieDoomed.dll DoomCheck.cs DoomedLoopUnrolling.cs DoomedStrategy.cs DoomErrorHandler.cs HasseDiagram.cs VCDoomed.cs obj/Debug/.NETFramework,Version=v4.5.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /reference:/usr/lib/mono/4.5-api/System.dll /reference:/usr/lib/mono/4.5-api/System.Xml.Linq.dll /reference:/usr/lib/mono/4.5-api/System.Data.DataSetExtensions.dll /reference:/usr/lib/mono/4.5-api/Microsoft.CSharp.dll /reference:/usr/lib/mono/4.5-api/System.Data.dll /reference:/usr/lib/mono/4.5-api/System.Xml.dll /reference:/usr/lib/mono/4.5-api/System.Core.dll /reference:/home/incal/dafny-dafny/boogie/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/home/incal/dafny-dafny/boogie/Source/CodeContractsExtender/bin/Checked//BoogieCodeContractsExtender.dll /reference:/home/incal/dafny-dafny/boogie/Source/Core/bin/Checked//BoogieCore.dll /reference:/home/incal/dafny-dafny/boogie/Source/Graph/bin/Checked//BoogieGraph.dll /reference:/home/incal/dafny-dafny/boogie/Binaries//BoogieModel.dll /reference:/home/incal/dafny-dafny/boogie/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/home/incal/dafny-dafny/boogie/Source/VCExpr/bin/Checked//BoogieVCExpr.dll /reference:/home/incal/dafny-dafny/boogie/Source/VCGeneration/bin/Checked//BoogieVCGeneration.dll /reference:/usr/lib/mono/4.5-api//mscorlib.dll /warn:4 Error: Garbage collector could not allocate 67108864 bytes of memory for nursery. /usr/lib/mono/xbuild/14.0/bin/Microsoft.CSharp.targets: error : Compiler crashed with code: 1. Task "Csc" execution -- FAILED Done building target "CoreCompile" in project "/home/incal/dafny-dafny/boogie/Source/Doomed/Doomed.csproj".-- FAILED Done building project "/home/incal/dafny-dafny/boogie/Source/Doomed/Doomed.csproj".-- FAILED Task "MSBuild" execution -- FAILED Done building target "Build" in project "/home/incal/dafny-dafny/boogie/Source/Boogie.sln".-- FAILED Done building project "/home/incal/dafny-dafny/boogie/Source/Boogie.sln".-- FAILED

Build FAILED. Errors:

/home/incal/dafny-dafny/boogie/Source/Boogie.sln (default targets) -> (Build target) -> /home/incal/dafny-dafny/boogie/Source/Doomed/Doomed.csproj (default targets) -> /usr/lib/mono/xbuild/14.0/bin/Microsoft.CSharp.targets (CoreCompile target) ->

/usr/lib/mono/xbuild/14.0/bin/Microsoft.CSharp.targets: error : Compiler crashed with code: 1.

0 Warning(s) 1 Error(s)

Time Elapsed 00:00:43.3560220

--
underground experts united 
http://user.it.uu.se/~embe8573

You ran out of memory.

--
https://www.greenend.org.uk/rjk/

Does that mean it cannot be done on a Pi? I don't have a lot of stuff running in the background, just Emacs, tmux, xterm. Hm, perhaps I could try it without running X...

--
underground experts united 
http://user.it.uu.se/~embe8573

Unbelievable! It worked when I didn't have X running. Ha ha ha - programmers at work :) But thanks a lot, let's hope the rest of the installation doesn't run into more issues...

--
underground experts united 
http://user.it.uu.se/~embe8573

Unfortunately, after building boogie, dafny wasn't as fortunate:

xbuild tool is deprecated and will be removed in future updates, use msbuil d instead /usr/lib/mono/xbuild/14.0/bin/Microsoft.CSharp.targets (CoreCompile target) ->

Rewriter.cs(1224): error CS0103: The name 'e' does not exist in the curren t context Parser.cs(3521): error CS0103: The name 'e' does not exist in the current context Parser.cs(3520): error CS0177: The out parameter 'e' must be assigned to b efore control leaves the current method

0 Warning(s) 3 Error(s)

Time Elapsed 00:00:20.9710930

--
underground experts united 
http://user.it.uu.se/~embe8573

Not running X will free up a lot of memory, but if that isn't enough try configuring a couple of GB of swap, and booking a holiday. Cross compiling on a larger linux box would be quicker.

---druck

--
This email has been checked for viruses by Avast antivirus software. 
https://www.avast.com/antivirus

I have realized that tho Raspbian is similar to Debian (a Debian fork) a lot of these more uncommon things would be a lot easier on a Debian on a stationary computer. However this is just a couple of assignment I have left from an education finished some 7 years ago, so I just want to do them to have nothing unfinished. So far I got by with a web tool to do dafny, but as it happened I Googled dafny to get to that interface, and stumbled across the repository and thought boy, it would be ten times the more pleasant workflow to have a real tool with my everyday editor. So I thought I'd try to do it, but if it doesn't work, it's not like I'm prepared to set up a whole new system just to have it.

--
underground experts united 
http://user.it.uu.se/~embe8573

To install Debian in a virtual machine it takes 15 minutes max (depending o n your internet connection speed).

Bye Jack

On Thu, 21 Sep 2017 01:32:27 +0200, Emanuel Berg declaimed the following:

Hook up a USB hard-drive, and configure a swap file on it... When done, disable swap file and remove the drive.

Actually, maybe put the entire development cycle on the hard drive too, then just save off (if it didn't install it automatically) the final results.

--
	Wulfraed                 Dennis Lee Bieber         AF6VN 
    wlfraed@ix.netcom.com    HTTP://wlfraed.home.netcom.com/

On Thu, 21 Sep 2017 04:15:55 -0700 (PDT), snipped-for-privacy@gmail.com declaimed the following:

It took more like 30-45 minutes for me -- using a three-DVD disk set I'd purchased, because my DSL would have taken weeks to download that (for the last month I've been lucky to obtain 900kbps -- lots of line noise on the phone; I'm hoping for a weather change to do something to the distribution box out in the trees)

--
	Wulfraed                 Dennis Lee Bieber         AF6VN 
    wlfraed@ix.netcom.com    HTTP://wlfraed.home.netcom.com/

But how much of that 12.4GB are you actually going to use? You can download a 290MB install image, then install what you actually need with apt-get. It used to take me all weekend to download a new CD distro on 56k dial-up, I'd just leave it running until it was done, and burn it on my

2x CD-R drive. Then computer magazines started putting the occasional Linux CD on the cover, and later DVDs with sometimes several CD distros per month. :-)

Emanuel Berg wrote:

I managed to install dafny with xbuild! This time, it was the disc space running out :)

However, dafny doesn't run.

There are a couple of binaries that will have to be chmod'd before anything can happen. The error messages, tho certainly not in a style I'm familiar with, gave great help with this.

However all said and done I got this, more cryptical message:

[ERROR] FATAL UNHANDLED EXCEPTION: System.AggregateException: One or more errors occurred. ---> System.IO.IOException: Write fault on path /home/incal/dafny-dafny/dafny/Binaries/[Unknown] at System.IO.FileStream.WriteInternal (System.Byte[] src, System.Int32 offset, System.Int32 count) [0x00077] in :0 at System.IO.FileStream.Write (System.Byte[] array, System.Int32 offset, System.Int32 count) [0x00090] in :0 at System.IO.StreamWriter.Flush (System.Boolean flushStream, System.Boolean flushEncoder) [0x0007e] in :0 at System.IO.StreamWriter.Write (System.Char[] buffer, System.Int32 index, System.Int32 count) [0x000d3] in :0 at System.IO.TextWriter.WriteLine (System.String value) [0x00070] in :0 at Microsoft.Boogie.SMTLib.SMTLibProcess.Send (System.String cmd) [0x00073] in :0 at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Send (System.String s, System.Boolean isCommon) [0x00033] in :0 at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.SendThisVC (System.String s) [0x00001] in :0 at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Reset (Microsoft.Boogie.VCExpressionGenerator gen) [0x0001b] in :0 at Microsoft.Boogie.Checker.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ProverInterface+ErrorHandler handler) [0x00025] in :0 at VC.VCGen+Split.BeginCheck (Microsoft.Boogie.Checker checker, Microsoft.Boogie.VerifierCallback callback, VC.ModelViewInfo mvInfo, System.Int32 no, System.Int32 timeout) [0x0022c] in :0 at VC.VCGen.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) [0x00724] in :0 at VC.ConditionGeneration.VerifyImplementation (Microsoft.Boogie.Implementation impl, System.Collections.Generic.List`1[Microsoft.Boogie.Counterexample]& errors, System.String requestId) [0x00019] in :0 at Microsoft.Boogie.ExecutionEngine.VerifyImplementation (Microsoft.Boogie.Program program, Microsoft.Boogie.PipelineStatistics stats, Microsoft.Boogie.ErrorReporterDelegate er, System.String requestId, System.Collections.Generic.Dictionary`2[TKey,TValue] extractLoopMappingInfo, Microsoft.Boogie.Implementation[] stablePrioritizedImpls, System.Int32 index, Microsoft.Boogie.ExecutionEngine+OutputCollector outputCollector, System.Collections.Generic.List`1[T] checkers, System.String programId) [0x00243] in :0 at Microsoft.Boogie.ExecutionEngine+c__DisplayClass27_2.b__5 (System.Object dummy) [0x00056] in :0 at System.Threading.Tasks.Task.InnerInvoke () [0x00025] in :0 at System.Threading.Tasks.Task.Execute () [0x00010] in :0 --- End of inner exception stack trace --- at System.AggregateException.Handle (System.Func`2[T,TResult] predicate) [0x00064] in :0 at Microsoft.Boogie.ExecutionEngine.InferAndVerify (Microsoft.Boogie.Program program, Microsoft.Boogie.PipelineStatistics stats, System.String programId, Microsoft.Boogie.ErrorReporterDelegate er, System.String requestId) [0x004e0] in :0 at Microsoft.Dafny.DafnyDriver.BoogiePipelineWithRerun (Microsoft.Boogie.Program program, System.String bplFileName, Microsoft.Boogie.PipelineStatistics& stats, System.String programId) [0x000bb] in :0 at Microsoft.Dafny.DafnyDriver.BoogieOnce (System.String baseFile, System.String moduleName, Microsoft.Boogie.Program boogieProgram, System.String programId, Microsoft.Boogie.PipelineStatistics& stats, Microsoft.Boogie.PipelineOutcome& oc) [0x00083] in :0 at Microsoft.Dafny.DafnyDriver.Boogie (System.String baseName, System.Collections.Generic.IEnumerable`1[T] boogiePrograms, System.String programId, System.Collections.Generic.Dictionary`2[System.String,Microsoft.Boogie.PipelineStatistics]& statss, Microsoft.Boogie.PipelineOutcome& oc) [0x0006e] in :0 at Microsoft.Dafny.DafnyDriver.ProcessFiles (System.Collections.Generic.IList`1[T] dafnyFiles, System.Collections.ObjectModel.ReadOnlyCollection`1[T] otherFileNames, Microsoft.Dafny.ErrorReporter reporter, System.Boolean lookForSnapshots, System.String programId) [0x00222] in :0 at Microsoft.Dafny.DafnyDriver.ThreadMain (System.String[] args) [0x0003a] in :0 at Microsoft.Dafny.DafnyDriver+c__DisplayClass1_0.b__0 () [0x00001] in :0 at System.Threading.ThreadHelper.ThreadStart_Context (System.Object state) [0x00014] in :0 at System.Threading.ExecutionContext.RunInternal (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state, System.Boolean preserveSyncCtx) [0x00071] in :0 at System.Threading.ExecutionContext.Run (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state, System.Boolean preserveSyncCtx) [0x00000] in :0 at System.Threading.ExecutionContext.Run (System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, System.Object state) [0x0002b] in :0 at System.Threading.ThreadHelper.ThreadStart () [0x00008] in :0

---> (Inner Exception #0) System.IO.IOException: Write fault on path /home/incal/dafny-dafny/dafny/Binaries/[Unknown] at System.IO.FileStream.WriteInternal (System.Byte[] src, System.Int32 offset, System.Int32 count) [0x00077] in :0 at System.IO.FileStream.Write (System.Byte[] array, System.Int32 offset, System.Int32 count) [0x00090] in :0 at System.IO.StreamWriter.Flush (System.Boolean flushStream, System.Boolean flushEncoder) [0x0007e] in :0 at System.IO.StreamWriter.Write (System.Char[] buffer, System.Int32 index, System.Int32 count) [0x000d3] in :0 at System.IO.TextWriter.WriteLine (System.String value) [0x00070] in :0 at Microsoft.Boogie.SMTLib.SMTLibProcess.Send (System.String cmd) [0x00073] in :0 at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Send (System.String s, System.Boolean isCommon) [0x00033] in :0 at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.SendThisVC (System.String s) [0x00001] in :0 at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Reset (Microsoft.Boogie.VCExpressionGenerator gen) [0x0001b] in :0 at Microsoft.Boogie.Checker.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ProverInterface+ErrorHandler handler) [0x00025] in :0 at VC.VCGen+Split.BeginCheck (Microsoft.Boogie.Checker checker, Microsoft.Boogie.VerifierCallback callback, VC.ModelViewInfo mvInfo, System.Int32 no, System.Int32 timeout) [0x0022c] in :0 at VC.VCGen.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) [0x00724] in :0 at VC.ConditionGeneration.VerifyImplementation (Microsoft.Boogie.Implementation impl, System.Collections.Generic.List`1[Microsoft.Boogie.Counterexample]& errors, System.String requestId) [0x00019] in :0 at Microsoft.Boogie.ExecutionEngine.VerifyImplementation (Microsoft.Boogie.Program program, Microsoft.Boogie.PipelineStatistics stats, Microsoft.Boogie.ErrorReporterDelegate er, System.String requestId, System.Collections.Generic.Dictionary`2[TKey,TValue] extractLoopMappingInfo, Microsoft.Boogie.Implementation[] stablePrioritizedImpls, System.Int32 index, Microsoft.Boogie.ExecutionEngine+OutputCollector outputCollector, System.Collections.Generic.List`1[T] checkers, System.String programId) [0x00243] in :0 at Microsoft.Boogie.ExecutionEngine+c__DisplayClass27_2.b__5 (System.Object dummy) [0x00056] in :0 at System.Threading.Tasks.Task.InnerInvoke () [0x00025] in :0 at System.Threading.Tasks.Task.Execute () [0x00010] in :0 (Inner Exception #1) System.IO.IOException: Write fault on path /home/incal/dafny-dafny/dafny/Binaries/[Unknown] at System.IO.FileStream.WriteInternal (System.Byte[] src, System.Int32 offset, System.Int32 count) [0x00077] in :0 at System.IO.FileStream.Write (System.Byte[] array, System.Int32 offset, System.Int32 count) [0x00090] in :0 at System.IO.StreamWriter.Flush (System.Boolean flushStream, System.Boolean flushEncoder) [0x0007e] in :0 at System.IO.StreamWriter.Write (System.Char[] buffer, System.Int32 index, System.Int32 count) [0x000d3] in :0 at System.IO.TextWriter.WriteLine (System.String value) [0x00070] in :0 at Microsoft.Boogie.SMTLib.SMTLibProcess.Send (System.String cmd) [0x00073] in :0 at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Send (System.String s, System.Boolean isCommon) [0x00033] in :0 at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.SendThisVC (System.String s) [0x00001] in :0 at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.Reset (Microsoft.Boogie.VCExpressionGenerator gen) [0x0001b] in :0 at Microsoft.Boogie.Checker.BeginCheck (System.String descriptiveName, Microsoft.Boogie.VCExprAST.VCExpr vc, Microsoft.Boogie.ProverInterface+ErrorHandler handler) [0x00025] in :0 at VC.VCGen+Split.BeginCheck (Microsoft.Boogie.Checker checker, Microsoft.Boogie.VerifierCallback callback, VC.ModelViewInfo mvInfo, System.Int32 no, System.Int32 timeout) [0x0022c] in :0 at VC.VCGen.VerifyImplementation (Microsoft.Boogie.Implementation impl, Microsoft.Boogie.VerifierCallback callback) [0x00724] in :0 at VC.ConditionGeneration.VerifyImplementation (Microsoft.Boogie.Implementation impl, System.Collections.Generic.List`1[Microsoft.Boogie.Counterexample]& errors, System.String requestId) [0x00019] in :0 at Microsoft.Boogie.ExecutionEngine.VerifyImplementation (Microsoft.Boogie.Program program, Microsoft.Boogie.PipelineStatistics stats, Microsoft.Boogie.ErrorReporterDelegate er, System.String requestId, System.Collections.Generic.Dictionary`2[TKey,TValue] extractLoopMappingInfo, Microsoft.Boogie.Implementation[] stablePrioritizedImpls, System.Int32 index, Microsoft.Boogie.ExecutionEngine+OutputCollector outputCollector, System.Collections.Generic.List`1[T] checkers, System.String programId) [0x00243] in :0 at Microsoft.Boogie.ExecutionEngine+c__DisplayClass27_2.b__5 (System.Object dummy) [0x00056] in :0 at System.Threading.Tasks.Task.InnerInvoke () [0x00025] in :0 at System.Threading.Tasks.Task.Execute () [0x00010] in :0

errors occurred. ---> System.IO.IOException: Write fault on path /home/inc al/dafny-dafny/dafny/Binaries/[Unknown]

It's not cryptical at all, it tells you exactly what happened. The fact that you can't understand what it tells you is completely another matter.

The best thing is to ask directly to dafny support.

Bye Jack

It tells me too much and too little. When something goes wrong one expects an error message, like in C, zsh, Lisp, or whatever, not a novel which cannot even say where it happened:

Write fault on path /home/incal/dafny-dafny/dafny/Binaries/[Unknown]

I'm starting to thing this whole Mono idea stinks as much as dafny. The fact that you defend it in an unpleasant way just makes my initial hunch all the stronger. I think I'll just use the ridiculous web interface, be done with it, and never look back.

--
underground experts united 
http://user.it.uu.se/~embe8573

Go on, then, what actually happened? Specifically, what system call was issued and what errno value was returned?

I?ve poked around inside the implementation of Mono, so I know where to look to get an answer. I?d agree with ?cryptical?, though: an error message that requires the reader to study a language runtime in order to comprehend it is in no way clear.

--
https://www.greenend.org.uk/rjk/

a scritto:

ere to

, though: an error

the issue is that it tries to write at a location and for some reason it ca n't and the exception is not handled correctly: programmer fault. And probably the user did something wrong when installing the program.

Or a "segmentation fault" or "Exit with error 3" would have been better?

Bye Jack

Indeed a stack backtrace is not an error message, it is evidence of a failure to anticipate, test for and handle the error - IOW evidence of poor and lazy programming.

--
Steve O'Hara-Smith                          |   Directable Mirror Arrays 
C:>WIN                                      | A better way to focus the sun 
The computer obeys and wins.                |    licences available see 
You lose and Bill collects.                 |    http://www.sohara.org/

It?s not writing to a location, it?s writing to a pipe or socket. The ?some reason? is that the other endpoint of the pipe has been closed.

The filename in the diagnostic is not just cryptic, it is misleading, since it?s unrelated to what actually went wrong.

--
https://www.greenend.org.uk/rjk/