Bug#852645: dafny: FTBFS

[Benjamin Barenblat]

1.9.8 builds fine, but that’s a 30,000-plus-LoC diff from 1.9.7, so
trying to get the new version into Stretch seems unlikely at this
point. I suspect cherry-picking upstream’s
dc724533490f66bb553d71be1b971f2008318adc and
e7cfcf3eb135c378d12c04f35d9f85f6cb241467 commits into 1.9.7 would be
sufficient, but I don’t have time to check right now. I’ll continue to
investigate and attempt to backport a fix.

Bug#852645: dafny: FTBFS

[Benjamin Barenblat]

I'm looking at this now.

Bug#852645: dafny: FTBFS

[Benjamin Barenblat]

I’m still planning to look at this, though I haven’t had the chance yet.

Bug#852645: dafny: FTBFS

[Benjamin Barenblat]

Thanks for looking into this.  You’re right – it looks like Dafny’s
having some trouble linking against Boogie.  The Dafny build process
statically links Boogie into Dafny; that’s why

cp -a /usr/lib/boogie/* Binaries
mkdir -p Source/Dafny/bin/Checked
cp -a /usr/lib/boogie/* Source/Dafny/bin/Checked

appears before the `xbuild` command.  However, Boogie builds fine and
is listed as a `Build-Depends-Indep` of Dafny, so I’m not entirely
sure what’s going on.

If you’d like to experiment with this, you can grab the relevant source from

https://benjamin.barenblat.name/git/debian-boogie.git
https://benjamin.barenblat.name/git/debian-dafny.git

Otherwise, I’ll try to have a look this weekend.

Bug#852645: dafny: FTBFS

[Roger Shimizu]

Dear Benjamin,

I see this issue on RC bug list, so I'm trying to help.
(Though I don't have much knowledge on mono ...)

Seems FTBFS caused by lack of some mono libraries?
So I guess there's something missing in Build-Depends in d/control?

PS. This package has never been built on buildd.
You should try source upload to prevent this.
Thanks!

Cheers,
-- 
Roger Shimizu, GMT +9 Tokyo
PGP/GPG: 4096R/6C6ACD6417B3ACB1

Bug#852645: dafny: FTBFS

[Santiago Vila]

Package: src:dafny
Version: 1.9.7-1
Severity: serious

Dear maintainer:

I tried to build this package in stretch with "dpkg-buildpackage -A"
but it failed:


[...]
 debian/rules build-indep
dh build-indep --with cli
   dh_testdir -i
   dh_update_autotools_config -i
   dh_auto_configure -i
   debian/rules override_dh_auto_build
make[1]: Entering directory '/<>'
cp -a /usr/lib/boogie/* Binaries
mkdir -p Source/Dafny/bin/Checked
cp -a /usr/lib/boogie/* Source/Dafny/bin/Checked
xbuild Source/Dafny.sln
XBuild Engine Version 14.0
Mono, Version 4.6.2.0
Copyright (C) 2005-2013 Various Mono authors

[... snipped ...]

Resolver.cs(2197,57): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(2871,44): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(3394,41): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(4399,82): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(4932,29): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(4940,29): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(4968,49): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(5114,37): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(5598,28): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(6255,45): error CS0246: The type or namespace name `Boogie' 
could not be found. Are you missing an assembly reference?
Resolver.cs(7070,38): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(7197,23): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(7300,30): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(7394,56): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(7525,47): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(7536,51): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(8316,38): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(8316,95): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(8552,40): error CS0246: The type or namespace name `Boogie' 
could not be found. Are you missing an assembly reference?
Resolver.cs(9085,59): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(9379,35): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(845,29): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(853,35): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(2250,16): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(2253,53): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(2543,34): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(3311,43): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(3435,28): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(9448,23): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Resolver.cs(9460,36): error CS0246: The type or namespace name `IToken' 
could not be found. Are you missing an assembly reference?
Rewriter.cs(34,31): error CS0246: The type or namespace name `Boogie' 
could not be found. Are