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.

Reply via email to