Armaël Guéneau

You didn't write in the PR message what `ShallowModel` and `DeepModel` get renamed into. It looks like the current choice is `View` and `EqModel`. This sounds fine to me, but...

Thinking about it a bit more this morning: what about `View` and `DeepModel`?

Regarding naming, I'm wondering if we should leave the logic functions as before with their intuitive names, and have `*_ghost` functions for the ones in the ghost code. (With the...

A `Debug`-specific hack could be to simply for Creusot to skip any implementation of `Debug` and assume a trivial spec (`#[ensures(true)]`). This would not require supporting `dyn`, and I don't...

Building Z3 ourselves could be a solution indeed (either on an old-enough ubuntu, or statically linking everything using musl with alpine). Alternatively, as a low effort hack, I wonder if...

with `println!("Hello world!")`, I get the following: ``` warning: support for string types is limited and experimental --> src/main.rs:6:14 | 6 | println!("Hello world!"); | ^^^^^^^^^^^^^^ | = note: `#[warn(creusot::experimental)]`...

Sorry if this unrelated, but I remember stumbling on an issue that looks similar, *on Linux*. Context: some time ago I was trying to do Rust-OCaml FFI bindings to build...

Here it is, I think: ``` $ cat t.ml open Zip $ ocamlfind ocamlopt -package camlzip -verbose -linkpkg -output-complete-obj -o foo.o t.ml Effective set of compiler predicates: pkg_unix,pkg_zip,pkg_camlzip,autolink,native + ocamlopt.opt...

I'm noticing a related issue, with (in a fresh switch with ocaml-base-compiler.4.13.0): ``` $ opam install graphics.5.1.2 ocamlfind.1.9.1 ocamlfind-secondary.1.9.1 dune.2.9.1 [ERROR] Package conflict! The actions to process have cyclic dependencies:...

Ah! I see. So at least part of the bug is that dune is considered as depending on ocamlfind-secondary, but this is not actually the case, as we have ocaml...