Make Z3 an optional dependency #223
Conversation
If Catala is compiled without Z3, trying to run it with the backend `Proof` will yield: ``` [ERROR] This instance of Catala was compiled without Z3 support. ``` and return 124 Note that this doesn't change the `make depends`, opam file or CI to account for it, it just enables it at the build-system level. There are also no hooks at this moment to have Catala self-document the options whith which it was compiled (e.g. in the `--help` screen). But that could be added in a more general way later, it's probably not really needed yet.
There was a problem hiding this comment.
Amazing! Altough I would prefer if you didn't rename the z3backend.ml into the z3backend.real.ml, the "realness" is implicit enough I guess.
Also could you provide some documentation about what dune command to run? Maybe create a new target in the top-level Makefile ?
It's exactly what I tried to do at first… but dune enforces it unfortunately 🤷
well it's not changed, just running |
|
Yeah an explicit |
|
BTW this should also fix #207, you might want to use the |
Also the CI will no longer compile/use z3
|
hm wait the CI still installs z3 |
and adapt the CI to skip z3 installation. Is it more usual for `all` targets to build everything but not include dependencies handling ?
denismerigoux
added
✨ enhancement
| (select | ||
| z3backend.ml | ||
| from | ||
| (z3 -> z3backend.real.ml) |
There was a problem hiding this comment.
Can you here make the case disjunction based on the fact that the user has passed a particular compilation flag or profile?
There was a problem hiding this comment.
Hum reading https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies it looks like you can't. But OK I thinking about it I quite like this behaviour : by default Catala does not come with the proof platform unless you have specifically installed z3 to enable it. Looks good to me!
|
So there are two types of CI: |
| (select | ||
| z3backend.ml | ||
| from | ||
| (z3 -> z3backend.real.ml) |
There was a problem hiding this comment.
Hum reading https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies it looks like you can't. But OK I thinking about it I quite like this behaviour : by default Catala does not come with the proof platform unless you have specifically installed z3 to enable it. Looks good to me!
Makefile
Outdated
| @@ -15,15 +15,20 @@ K := $(foreach exec,$(EXECUTABLES),\ | |||
| $(if $(shell which $(exec)),some string,$(warning [WARNING] No "$(exec)" executable found. \ | |||
| Please install this executable for everything to work smoothly))) | |||
|
|
|||
| dependencies-ocaml: | |||
| dependencies-ocaml-noz3: | |||
There was a problem hiding this comment.
OK thinking about it the default should not include z3 and the special target should be dependencies-ocaml-with-z3:)
If Catala is compiled without Z3, trying to run it with the backend
Proofwill yield:
and return 124
Note that this doesn't change the
make depends, opam file or CI to accountfor it, it just enables it at the build-system level.
There are also no hooks at this moment to have Catala self-document the
options whith which it was compiled (e.g. in the
--helpscreen). But thatcould be added in a more general way later, it's probably not really needed
yet.