add Dockerfile

[kidq330]

Closes #962

Here's what I hacked up - some tests fail, is that a known issue?

I was thinking about a simple GH action to build + test the image, as a follow-up to this PR, though there is some useful CI set up already.

[kidq330]

One of the tests in question:

normalized stderr:
error: internal compiler error: crates/flux-infer/src/fixpoint_encoding.rs:436:35: failed to run fixpoint: Custom { kind: UnexpectedEof, error: Error("EOF while parsing a value", line: 1, column: 0) }

thread 'rustc' panicked at crates/flux-infer/src/fixpoint_encoding.rs:436:35:
Box<dyn Any>
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
error: aborting due to 1 previous error




The actual stderr differed from the expected stderr.
Actual stderr saved to /tmp/compiletestHYLMmj/extern_specs/extern_spec_trait00.stage-id.stderr
To update references, rerun the tests and pass the `--bless` flag
To only update this specific test, also pass `--test-args extern_specs/extern_spec_trait00.rs`

error: 1 errors occurred comparing output.
status: exit status: 101
command: "../target/debug/rustc-flux" "tests/pos/extern_specs/extern_spec_trait00.rs" "-L" "/tmp/compiletestHYLMmj" "--target=x86_64-unknown-linux-gnu" "--error-format" "json" "-C" "prefer-dynamic" "-o" "/tmp/compiletestHYLMmj/extern_specs/extern_spec_trait00.stage-id" "-A" "unused" "--crate-type=rlib" "--edition=2021" "--emit=metadata" "-L" "/tmp/compiletestHYLMmj/extern_specs/extern_spec_trait00.stage-id.aux"
stdout:
------------------------------------------

------------------------------------------
stderr:
------------------------------------------
{"$message_type":"diagnostic","message":"crates/flux-infer/src/fixpoint_encoding.rs:436:35: failed to run fixpoint: Custom { kind: UnexpectedEof, error: Error(\"EOF while parsing a value\", line: 1, column: 0) }","code":null,"level":"error: internal compiler error","spans":[],"children":[],"rendered":"error: internal compiler error: crates/flux-infer/src/fixpoint_encoding.rs:436:35: failed to run fixpoint: Custom { kind: UnexpectedEof, error: Error(\"EOF while parsing a value\", line: 1, column: 0) }\n\n"}
thread 'rustc' panicked at crates/flux-infer/src/fixpoint_encoding.rs:436:35:
Box<dyn Any>
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
{"$message_type":"diagnostic","message":"aborting due to 1 previous error","code":null,"level":"error","spans":[],"children":[],"rendered":"error: aborting due to 1 previous error\n\n"}

------------------------------------------

test [ui] pos/extern_specs/extern_spec_trait00.rs ... FAILED

Since GH passed all tests I'd suspect this to be an issue with dependency versions

[kidq330]

Also, just changed from slim-bullseye to regular base image and stuck on test [ui] pos/surface/bitvec01.rs ... test [ui] pos/surface/bitvec01.rs has been running for over 60 seconds - I'm not sure yet if this isn't an issue in my setup so I'll revert to draft PR for now

[nilehmann]

Thanks @kidq330!

I only look at this superficially (I'll have more time tomorrow). The failing test may be related to z3's version. Do you know which versions is being installed? I've had problems with that in the past because some distros have old versions of z3

[kidq330]

@nilehmann bullseye offers z3 @ 4.8.10-1 and is the latest debian with an official Haskell image, which version would you suggest?
No rush with the review obvs. :)

[nilehmann]

We test in ci with 4.12 so that should work, although we should probably update everything to 4.13, so I'd say let's do that.

[nilehmann]

@kidq330 I took a more detailed look. It looks good. The only thing missing is to use a newer version of z3. I would use 4.13.4 (latest). If that's not available in the repo I guess the only alternative is to download one of the binary releases from github (https://github.com/Z3Prover/z3/releases/tag/z3-4.13.4)

[kidq330]

@nilehmann Unfortunately the standard debian/ubuntu apt repositories have pretty outdated versions of z3 (>4.8 for debian only since trixie/13 which is not widely used in docker yet)
Like you mentioned downloading the binary would probably be the most straightforward, there's also an ubuntu image, but it was last updated 4 months ago. I'll get to it when I have the time, hopefully to support both x64 and arm64