diff --git a/.github/workflows/run-builds.yml b/.github/workflows/run-builds.yml index ea4639c1..6f84f4c6 100644 --- a/.github/workflows/run-builds.yml +++ b/.github/workflows/run-builds.yml @@ -27,7 +27,7 @@ jobs: ./french_law/python/setup_env.sh - name: Install OCaml dependencies run: | - opam install . --deps-only --with-doc --with-test + make dependencies-ocaml-with-z3 - name: Make build run: | OCAMLRUNPARAM=b opam exec -- make build diff --git a/.github/workflows/run-make-all.yml b/.github/workflows/run-make-all.yml index aee61b76..5c9bb40b 100644 --- a/.github/workflows/run-make-all.yml +++ b/.github/workflows/run-make-all.yml @@ -19,4 +19,4 @@ jobs: clean: false - name: Make all run: | - OCAMLRUNPARAM=b opam exec -- make all -B + OCAMLRUNPARAM=b opam exec -- make dependencies all -B diff --git a/.nix/no-web.patch b/.nix/no-web.patch index 63d5547f..32a3cba7 100644 --- a/.nix/no-web.patch +++ b/.nix/no-web.patch @@ -1,33 +1,45 @@ diff --git a/compiler/catala_web_interpreter.ml b/compiler/catala_web_interpreter.ml deleted file mode 100644 -index 31d5289..0000000 +index cc842a5d..00000000 --- a/compiler/catala_web_interpreter.ml +++ /dev/null -@@ -1,16 +0,0 @@ +@@ -1,28 +0,0 @@ -open Driver -open Js_of_ocaml - -let _ = - Js.export_all - (object%js -- method interpret (contents : Js.js_string Js.t) (scope : Js.js_string Js.t) -- (language : Js.js_string Js.t) (trace : bool) = +- method interpret +- (contents : Js.js_string Js.t) +- (scope : Js.js_string Js.t) +- (language : Js.js_string Js.t) +- (trace : bool) = - driver - (Contents (Js.to_string contents)) -- false false false false "Interpret" -- (Some (Js.to_string language)) -- None trace false false -- (Some (Js.to_string scope)) -- None +- { +- Utils.Cli.debug = false; +- unstyled = false; +- wrap_weaved_output = false; +- avoid_exceptions = false; +- backend = "Interpret"; +- language = Some (Js.to_string language); +- max_prec_digits = None; +- trace = false; +- disable_counterexamples = false; +- optimize = false; +- ex_scope = Some (Js.to_string scope); +- output_file = None; +- } - end) diff --git a/compiler/dune b/compiler/dune -index d192291..994c528 100644 +index 2c5a1996..f6c38809 100644 --- a/compiler/dune +++ b/compiler/dune -@@ -10,16 +10,6 @@ +@@ -19,16 +19,6 @@ (libraries calendar zarith zarith_stubs_js) (modules runtime)) - + -(executable - (name catala_web_interpreter) - (modes byte js) @@ -40,4 +52,4 @@ index d192291..994c528 100644 - (executable (name catala) - (modes native) \ No newline at end of file + (modes native js) diff --git a/INSTALL.md b/INSTALL.md index 2f10b48a..662ce87a 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -58,6 +58,11 @@ git submodules, with This should ensure everything is set up for developing on the Catala compiler! +**Warning**: this command does not include the `z3` dependency required to enable +the proof platform feature of Catala. If you wish to enable support for the +proof platform and the `Proof` command of the Catala compiler, you should +instead execute `make dependencies-with-ocaml` prior to building the compiler. + Other features of the Catala repository also require the following executables to be present diff --git a/Makefile b/Makefile index 35eed77d..58ca1393 100644 --- a/Makefile +++ b/Makefile @@ -18,15 +18,20 @@ K := $(foreach exec,$(EXECUTABLES),\ dependencies-ocaml: opam install . --deps-only --with-doc --with-test --yes +dependencies-ocaml-with-z3: + opam install . z3 --deps-only --with-doc --with-test --yes + dependencies-js: $(MAKE) -C $(FRENCH_LAW_JS_LIB_DIR) dependencies init-submodules: git submodule update --init + #> dependencies : Install the Catala OCaml, JS and Git dependencies dependencies: dependencies-ocaml dependencies-js init-submodules +dependencies-with-z3: dependencies-ocaml-with-z3 dependencies-js init-submodules ########################################## # Catala compiler rules @@ -285,7 +290,7 @@ catala.html: $(COMPILER_DIR)/utils/cli.ml | tac | sed "1,20d" | tac > $@ #> website-assets : Builds all the assets necessary for the Catala website -website-assets: doc literate_examples grammar.html catala.html js_build build_french_law_library_js +website-assets: doc literate_examples grammar.html catala.html build_french_law_library_js ########################################## # Misceallenous @@ -293,7 +298,7 @@ website-assets: doc literate_examples grammar.html catala.html js_build build_fr #> all : Run all make commands all: \ - dependencies build doc website-assets\ + build doc website-assets\ tests \ generate_french_law_library_ocaml build_french_law_library_ocaml \ tests_ocaml bench_ocaml \ diff --git a/build_system/clerk_driver.ml b/build_system/clerk_driver.ml index c0d5fe7e..015fbc0b 100644 --- a/build_system/clerk_driver.ml +++ b/build_system/clerk_driver.ml @@ -130,21 +130,6 @@ let info = (**{1 Testing}*) -let catala_backend_to_string (backend : Cli.backend_option) : string = - match backend with - | Cli.Dcalc -> "Dcalc" - | Cli.Html -> "Html" - | Cli.Interpret -> "Interpret" - | Cli.Latex -> "Latex" - | Cli.Lcalc -> "Lcalc" - | Cli.Makefile -> "Makefile" - | Cli.OCaml -> "OCaml" - | Cli.Proof -> "Proof" - | Cli.Python -> "Python" - | Cli.Scalc -> "Scalc" - | Cli.Scopelang -> "Scopelang" - | Cli.Typecheck -> "Typecheck" - type expected_output_descr = { base_filename : string; output_dir : string; @@ -421,7 +406,8 @@ let collect_all_ninja_build let vars = [ ( "catala_cmd", - Nj.Expr.Lit (catala_backend_to_string expected_output.backend) + Nj.Expr.Lit + (Cli.catala_backend_option_to_string expected_output.backend) ); ("tested_file", Nj.Expr.Lit tested_file); ( "expected_output", @@ -429,12 +415,9 @@ let collect_all_ninja_build (expected_output.output_dir ^ expected_output.complete_filename) ); ] - in - let output_build_kind = - if reset_test_outputs then "reset" else "test" - in - let catala_backend = - catala_backend_to_string expected_output.backend + and output_build_kind = if reset_test_outputs then "reset" else "test" + and catala_backend = + Cli.catala_backend_option_to_string expected_output.backend in let get_rule_infos ?(rule_postfix = "") : diff --git a/catala.opam b/catala.opam index 961545dd..e1270148 100644 --- a/catala.opam +++ b/catala.opam @@ -36,11 +36,14 @@ depends: [ "benchmark" {>= "1.6"} "js_of_ocaml-ppx" {>= "3.8.0"} "camomile" {>= "1.0.2"} - "z3" {>= "4.8.11"} "cppo" {>= "1"} "alcotest" {with-test & >= "1.5.0"} "odoc" {with-doc} ] +depopts: ["z3"] +conflicts: [ + "z3" {< "4.8.11"} +] build: [ ["dune" "subst"] {dev} [ diff --git a/compiler/driver.ml b/compiler/driver.ml index 75eab3a9..8af83607 100644 --- a/compiler/driver.ml +++ b/compiler/driver.ml @@ -62,22 +62,11 @@ let driver source_file (options : Cli.options) : int = Cli.locale_lang := language; let backend = options.backend in let backend = - let backend = String.lowercase_ascii backend in - if backend = "makefile" then Cli.Makefile - else if backend = "latex" then Cli.Latex - else if backend = "html" then Cli.Html - else if backend = "interpret" then Cli.Interpret - else if backend = "ocaml" then Cli.OCaml - else if backend = "dcalc" then Cli.Dcalc - else if backend = "scopelang" then Cli.Scopelang - else if backend = "python" then Cli.Python - else if backend = "proof" then Cli.Proof - else if backend = "typecheck" then Cli.Typecheck - else if backend = "lcalc" then Cli.Lcalc - else if backend = "scalc" then Cli.Scalc - else - Errors.raise_error - "The selected backend (%s) is not supported by Catala" backend + match Cli.catala_backend_option_of_string backend with + | Some b -> b + | None -> + Errors.raise_error + "The selected backend (%s) is not supported by Catala" backend in let prgm = Surface.Parser_driver.parse_top_level_file source_file language diff --git a/compiler/lcalc/ast.ml b/compiler/lcalc/ast.ml index 0d833598..c71bb70f 100644 --- a/compiler/lcalc/ast.ml +++ b/compiler/lcalc/ast.ml @@ -121,7 +121,8 @@ let make_none (pos : Pos.t) : expr Pos.marked Bindlib.box = let make_some (e : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box = let pos = Pos.get_position @@ Bindlib.unbox e in let mark : 'a -> 'a Pos.marked = Pos.mark pos in - let+ e = e in + let+ e = e [@ocamlformat "disable"] in + mark @@ EInj (e, 1, option_enum, [ (D.TLit D.TUnit, pos); (D.TAny, pos) ]) (** [make_matchopt_with_abs_arms arg e_none e_some] build an expression @@ -133,8 +134,7 @@ let make_matchopt_with_abs_arms (e_some : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box = let pos = Pos.get_position @@ Bindlib.unbox arg in let mark : 'a -> 'a Pos.marked = Pos.mark pos in - - let+ arg = arg and+ e_none = e_none and+ e_some = e_some in + let+ arg = arg and+ e_none = e_none and+ e_some = e_some [@ocamlformat "disable"] in mark @@ EMatch (arg, [ e_none; e_some ], option_enum) diff --git a/compiler/utils/cli.ml b/compiler/utils/cli.ml index fef4c457..f64ff46c 100644 --- a/compiler/utils/cli.ml +++ b/compiler/utils/cli.ml @@ -17,6 +17,50 @@ type backend_lang = En | Fr | Pl +type backend_option = + | Dcalc + | Html + | Interpret + | Latex + | Lcalc + | Makefile + | OCaml + | Proof + | Python + | Scalc + | Scopelang + | Typecheck + +let catala_backend_option_to_string = function + | Dcalc -> "Dcalc" + | Html -> "Html" + | Interpret -> "Interpret" + | Latex -> "Latex" + | Lcalc -> "Lcalc" + | Makefile -> "Makefile" + | OCaml -> "OCaml" + | Proof -> "Proof" + | Python -> "Python" + | Scalc -> "Scalc" + | Scopelang -> "Scopelang" + | Typecheck -> "Typecheck" + +let catala_backend_option_of_string backend = + match String.lowercase_ascii backend with + | "dcalc" -> Some Dcalc + | "html" -> Some Html + | "interpret" -> Some Interpret + | "latex" -> Some Latex + | "lcalc" -> Some Lcalc + | "makefile" -> Some Makefile + | "ocaml" -> Some OCaml + | "proof" -> Some Proof + | "python" -> Some Python + | "scalc" -> Some Scalc + | "scopelang" -> Some Scopelang + | "typecheck" -> Some Typecheck + | _ -> None + (** Source files to be compiled *) let source_files : string list ref = ref [] @@ -85,20 +129,6 @@ let backend = ~doc: "Backend selection (see the list of commands for available options).") -type backend_option = - | Dcalc - | Html - | Interpret - | Latex - | Lcalc - | Makefile - | OCaml - | Proof - | Python - | Scalc - | Scopelang - | Typecheck - let language = Arg.( value diff --git a/compiler/utils/cli.mli b/compiler/utils/cli.mli index a25fdbfb..b2da8f66 100644 --- a/compiler/utils/cli.mli +++ b/compiler/utils/cli.mli @@ -17,6 +17,28 @@ type backend_lang = En | Fr | Pl +type backend_option = + | Dcalc + | Html + | Interpret + | Latex + | Lcalc + | Makefile + | OCaml + | Proof + | Python + | Scalc + | Scopelang + | Typecheck + +val catala_backend_option_to_string : backend_option -> string +(** [catala_backend_to_string backend] returns the string representation of the + given [backend].*) + +val catala_backend_option_of_string : string -> backend_option option +(** [catala_backend_option_of_string backend] returns the {!type: + backend_option} corresponding to the [backend] string. *) + (** {2 Configuration globals} *) val source_files : string list ref @@ -50,21 +72,6 @@ val unstyled : bool Cmdliner.Term.t val trace_opt : bool Cmdliner.Term.t val wrap_weaved_output : bool Cmdliner.Term.t val backend : string Cmdliner.Term.t - -type backend_option = - | Dcalc - | Html - | Interpret - | Latex - | Lcalc - | Makefile - | OCaml - | Proof - | Python - | Scalc - | Scopelang - | Typecheck - val language : string option Cmdliner.Term.t val max_prec_digits_opt : int option Cmdliner.Term.t val ex_scope : string option Cmdliner.Term.t diff --git a/compiler/verification/dune b/compiler/verification/dune index 459abfed..0584a6c2 100644 --- a/compiler/verification/dune +++ b/compiler/verification/dune @@ -1,7 +1,17 @@ (library (name verification) (public_name catala.verification) - (libraries bindlib utils dcalc runtime z3 calendar)) + (libraries + bindlib + utils + dcalc + runtime + calendar + (select + z3backend.ml + from + (z3 -> z3backend.real.ml) + (-> z3backend.dummy.ml)))) (documentation (package catala) diff --git a/compiler/verification/z3backend.dummy.ml b/compiler/verification/z3backend.dummy.ml new file mode 100644 index 00000000..90beed67 --- /dev/null +++ b/compiler/verification/z3backend.dummy.ml @@ -0,0 +1,42 @@ +(* This file is part of the Catala compiler, a specification language for tax + and social benefits computation rules. Copyright (C) 2022 Inria, contributor: + Aymeric Fromherz + + Licensed under the Apache License, Version 2.0 (the "License"); you may not + use this file except in compliance with the License. You may obtain a copy of + the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, WITHOUT + WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the + License for the specific language governing permissions and limitations under + the License. *) + +(** Replicating the interface, with no actual implementation for compiling + without the expected backend. All functions print an error message and exit *) + +let dummy () = + Utils.Cli.error_print + "This instance of Catala was compiled without Z3 support."; + exit 124 + +module Io = struct + let init_backend () = dummy () + + type backend_context = unit + + let make_context _ _ = dummy () + + type vc_encoding = unit + + let translate_expr _ _ = dummy () + + type model = unit + type vc_encoding_result = Success of model * model | Fail of string + + let print_positive_result _ = dummy () + let print_negative_result _ _ _ = dummy () + let encode_and_check_vc _ _ = dummy () +end diff --git a/compiler/verification/z3backend.ml b/compiler/verification/z3backend.real.ml similarity index 100% rename from compiler/verification/z3backend.ml rename to compiler/verification/z3backend.real.ml diff --git a/default.nix b/default.nix index 1aec5238..0ae0adfd 100644 --- a/default.nix +++ b/default.nix @@ -21,6 +21,7 @@ , cppo , ppx_deriving , z3 +, alcotest , menhirLib ? null #for nixos-unstable compatibility. }: @@ -57,6 +58,8 @@ buildDunePackage rec { ppx_deriving + alcotest + unionfind bindlib ] ++ (if isNull menhirLib then [ ] else [ menhirLib ]); diff --git a/dune-project b/dune-project index 4facb1cb..3e8ad6ed 100644 --- a/dune-project +++ b/dune-project @@ -68,8 +68,6 @@ (>= 3.8.0)) (camomile (>= 1.0.2)) - (z3 - (>= 4.8.11)) (cppo (>= 1)) (obelisk :dev) @@ -80,7 +78,11 @@ (ocamlformat (and :dev - (= 0.20.1))))) + (= 0.20.1)))) + (depopts + z3) + (conflicts + (z3 (< 4.8.11)))) (package (name french_law)