search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.94k stars 263 forks source link

Linux binary build has a number issues #185

Closed HuStmpHrrr closed 6 years ago

HuStmpHrrr commented 6 years ago

I was install Dafny on my system:

$ uname -a
Linux 3NXDOMAIN 4.13.0-36-generic #40~16.04.1-Ubuntu SMP Fri Feb 16 23:25:58 UTC 2018 x86_64 x86_64 x86_64 GNU/Linux

and I downloaded this version: https://github.com/Microsoft/dafny/releases/tag/v2.1.1

And to make it run, I have discovered following issues:

  1. both dafny and dafny-server is not executable by default. Therefore I need to do chmod +x myself. This is not a problem for most of the linux users, but it's something good to have.

  2. dafny is coded up in windows environment, therefore when executing it in Linux environment, it inevitably has following issue:

$ dafny
/usr/bin/env: ‘bash\r’: No such file or directory

I will need to run dos2unix to fix both dafny and dafny-server. This is also not a big deal for most of the users, but still something very good to have.

  1. when creating symlink from another folder to dafny and executing it from there will create an issue, due to how the script is coded up:
$ dafny
Error: Dafny.exe not found at /home/zs2hu/tools/local/bin/Dafny.exe.

The reason for that is the following line:

DAFNY=$(dirname "${BASH_SOURCE[0]}")/Dafny.exe

When creating symlink, ${BASH_SOURCE[0]} points to the symlink instead of the real location of the file, hence the error. I personally fixed it in following way:

DAFNY=$(dirname `readlink -f "${BASH_SOURCE[0]}"`)/Dafny.exe

It should work for most of the modern linux systems. However, I am not sure how portable is that. I believe, for example, in Solaris system, readlink does not have -f option. Do you guys good with fix like that?

HuStmpHrrr commented 6 years ago

I created a PR for the third point: https://github.com/Microsoft/dafny/pull/186

However, I don't think point 1 and 2 are the problem from source code. Is the build built on a Windows machine? that would be the problem.

HuStmpHrrr commented 6 years ago

Hi, thank you for merging.

Could someone know the building process comment on point 1 and 2?

jamesbornholt commented 6 years ago

I believe I fixed (2) after the latest release (see c9f52fe), so that should work for the next version. For (1), the packaging script does try to add the executable bit to those scripts, but it doesn't seem to stick (at least on my Mac). I'll experiment with that some more.

HuStmpHrrr commented 6 years ago

@jamesbornholt is the packaging script https://github.com/Microsoft/dafny/blob/master/package.py ?

jamesbornholt commented 6 years ago

Yep. Line 147 is the magic line. And, as you suspected, it gets run on Windows.

HuStmpHrrr commented 6 years ago

The problem is the permission bits should be 0100777 << 16. also the next line of reading file contents is suspicious.

the permission bits should be 0100777 << 16

or not. I am not sure then. one needs to test it on a windows machine to know what's happening.

HuStmpHrrr commented 6 years ago

The permission bits, unfortunately, actually got into the zip file. it's just for some reason, when uncompressing, the bits are not recovered. I can confirm that because I can see the bits set in the hex dump of the zip file:

02676d30: 2e70 6462 504b 0102 1400 1400 0000 0800  .pdbPK..........
02676d40: 136a 8c4b c0dd a18e d900 0000 4b01 0000  .j.K........K...
02676d50: 0b00 0000 0000 0000 0000 0000 ff01 6b78  ..............kx
02676d60: 0602 6461 666e 792f 6461 666e 7950 4b01  ..dafny/dafnyPK.

this row

02676d50: 0b00 0000 0000 0000 0000 0000 ff01 6b78  ..............kx

the 4 bytes 0000 ff01 exactly encodes 0777 permission, i.e. the higher 2 bytes of the external file attribute is 0x01ff. according to standard https://pkware.cachefly.net/webdocs/casestudies/APPNOTE.TXT section 4.3.12, this encodes as intended. I am uncertain what caused the permission bits unset after decompression. it's either due to the file head which says file is compressed in MS instead of UNIX, or otherwise it's a bug in unzip.

jamesbornholt commented 6 years ago

This should be fixed in the packaging script now, so the next binary release should work fine (I just tested by packaging on Windows and extracting on both Linux and macOS).

I also updated the fix from #186 to be portable to macOS (and other BSDs I guess), which doesn't support the -f flag to readlink.

Thanks for the report!

HuStmpHrrr commented 6 years ago

oh wow. so it's indeed the OS flag. good to know such quirk exists.