Emanuel Berg wrote:

>>>> Error: Garbage collector could not
>>>> allocate 67108864 bytes of memory
>>>> for nursery.
>>>
>>> You ran out of memory.
>>
>> 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...
>
> 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...

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

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 21/09/2017 03:33:22.
__________________________________________________
Project "/home/incal/dafny-dafny/dafny/Source/Dafny.sln" (default target(s)):
 Target ValidateSolutionConfiguration:
  Building solution configuration "Checked|Mixed Platforms".
 Target Build:
  Project
"/home/incal/dafny-dafny/dafny/Source/DafnyRuntime/DafnyRuntime.csproj"
(default target(s)):
   Target PrepareForBuild:
    Configuration: Release 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/dafny/Source/DafnyRuntime/DafnyRuntime.csproj".
  Project "/home/incal/dafny-dafny/dafny/Source/Dafny/DafnyPipeline.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:
    Tool /usr/lib/mono/4.5/csc.exe execution started with arguments: /noconfig
/debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign
/out:obj/Checked/DafnyPipeline.dll Cloner.cs Reporting.cs
Triggers/QuantifiersCollection.cs Triggers/
QuantifierSplitter.cs Triggers/TriggerExtensions.cs
Triggers/QuantifiersCollector.cs Triggers/TriggersCollector.cs
Triggers/TriggerUtils.cs Util.cs Compiler.cs BigIntegerParser.cs DafnyAst.cs
DafnyMain.cs DafnyOptions.cs Printer.cs RefinementTransformer.
cs Resolver.cs Rewriter.cs SccGraph.cs Translator.cs ../version.cs cce.cs
Parser.cs Scanner.cs
obj/Checked/.NETFramework,Version=v4.5.AssemblyAttribute.cs /target:library
/define:"TRACE;DEBUG;NO_ENABLE_IRONDAFNY" /nostdlib /platform:AnyCPU
/reference:../.
./../boogie/Binaries/BoogieBasetypes.dll
/reference:../../../boogie/Binaries/BoogieCore.dll
/reference:../../../boogie/Binaries/BoogieParserHelper.dll
/reference:/usr/lib/mono/4.5-api/System.dll
/reference:/usr/lib/mono/4.5-api/System.Numerics.dll /
reference:/usr/lib/mono/4.5-api/System.Core.dll
/reference:/home/incal/dafny-dafny/dafny/Binaries//DafnyRuntime.dll
/reference:/usr/lib/mono/4.5-api//mscorlib.dll
    Microsoft (R) Visual C# Compiler version 2.3.0.61801 (3722bb71)
    Copyright (C) Microsoft Corporation. All rights reserved.
Rewriter.cs(1224): error CS0103: The name 'e' does not exist in the current
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 before
control leaves the current method
   Task "Csc" execution -- FAILED
   Done building target "CoreCompile" in project
"/home/incal/dafny-dafny/dafny/Source/Dafny/DafnyPipeline.csproj".-- FAILED
  Done building project
"/home/incal/dafny-dafny/dafny/Source/Dafny/DafnyPipeline.csproj".-- FAILED
 Task "MSBuild" execution -- FAILED
 Done building target "Build" in project
"/home/incal/dafny-dafny/dafny/Source/Dafny.sln".-- FAILED
Done building project "/home/incal/dafny-dafny/dafny/Source/Dafny.sln".--
FAILED

Build FAILED.
Errors:

/home/incal/dafny-dafny/dafny/Source/Dafny.sln (default targets) ->
(Build target) ->
/home/incal/dafny-dafny/dafny/Source/Dafny/DafnyPipeline.csproj (default
targets) ->
/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 current
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
before 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

--- SoupGate-Win32 v1.05