dafny on R-Pi

Did anyone manage to get dafny running on a Pi?
I'm on Raspbian 8. Mono 5.2.
I got to the "xbuild" step, then it just crashed
over and over.
Here is the software:
formatting link

--
underground experts united 
http://user.it.uu.se/~embe8573
Reply to
Emanuel Berg
Loading thread data ...
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/
Reply to
Richard Kettlewell
--
underground experts united 
http://user.it.uu.se/~embe8573
Reply to
Emanuel Berg
You ran out of memory.
--
https://www.greenend.org.uk/rjk/
Reply to
Richard Kettlewell
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
Reply to
Emanuel Berg
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
Reply to
Emanuel Berg
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
Reply to
Emanuel Berg
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
Reply to
druck
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
Reply to
Emanuel Berg
To install Debian in a virtual machine it takes 15 minutes max (depending o n your internet connection speed).
Bye Jack
Reply to
jack4747
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/
Reply to
Dennis Lee Bieber
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/
Reply to
Dennis Lee Bieber
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. :-)
Reply to
Rob Morley
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
Reply to
Emanuel Berg
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
Reply to
jack4747
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
Reply to
Emanuel Berg
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/
Reply to
Richard Kettlewell
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
Reply to
jack4747
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 
 Click to see the full signature
Reply to
Ahem A Rivet's Shot
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/
Reply to
Richard Kettlewell

ElectronDepot website is not affiliated with any of the manufacturers or service providers discussed here. All logos and trade names are the property of their respective owners.