diff --git a/.github/workflows/build_docker.yml b/.github/workflows/build_docker.yml index 328ddee96..a975ed853 100644 --- a/.github/workflows/build_docker.yml +++ b/.github/workflows/build_docker.yml @@ -22,13 +22,20 @@ jobs: image: ocamlpro/ocaml:4.10 steps: + # Checkout the code of the current branch + - name: Checkout code + uses: actions/checkout@v3 + + # Switch to ocaml user + - run: su ocaml + # This line is needed to acces and use opam. We are unable to set the user # to `ocaml` with the container parameters - run: sudo chmod a+wx . - # Checkout the code of the current branch - - name: Checkout code - uses: actions/checkout@v2 + # This line is needed to allow the working directory to be used even + # the ocaml user do not have rights on it. + - run: CURRENTDIR=$(basename $(pwd)); git config --global --add safe.directory /__w/$CURRENTDIR/$CURRENTDIR # Create a switch with the system compiler (no compilation needed). # And then, install external (no need for depext with opam 2.1) and libs deps. diff --git a/.github/workflows/build_js.yml b/.github/workflows/build_js.yml index 80e4a97f9..2d802c22b 100644 --- a/.github/workflows/build_js.yml +++ b/.github/workflows/build_js.yml @@ -24,7 +24,7 @@ jobs: steps: # Checkout the code of the current branch - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 # Update apt-get database - name: Update apt-get database @@ -44,9 +44,9 @@ jobs: # Get an OCaml environment with opam installed and the proper ocaml version # opam will used opam cache environment if retrieved - name: Use OCaml ${{ env.OCAML_DEFAULT_VERSION }} - uses: avsm/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v2 with: - ocaml-version: ${{ env.OCAML_DEFAULT_VERSION }} + ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }} # Pin the packages, this is needed for opam depext # remove this step when opam 2.1 will be used diff --git a/.github/workflows/build_macos.yml b/.github/workflows/build_macos.yml index 14cd4156e..3e3c4d109 100644 --- a/.github/workflows/build_macos.yml +++ b/.github/workflows/build_macos.yml @@ -31,7 +31,7 @@ jobs: steps: # Checkout the code of the current branch - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 # Retrieve the opam cache with unique key # A new cache is created/used if the `.opam` files changes or @@ -47,9 +47,9 @@ jobs: # Get an OCaml environment with opam installed and the proper ocaml version # opam will used opam cache environment if retrieved - name: Use OCaml ${{ env.OCAML_DEFAULT_VERSION }} - uses: avsm/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v2 with: - ocaml-version: ${{ env.OCAML_DEFAULT_VERSION }} + ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }} # Pin the packages, this is needed for opam depext # remove this step when opam 2.1 will be used diff --git a/.github/workflows/build_make.yml b/.github/workflows/build_make.yml index a5345b5e6..13768389a 100644 --- a/.github/workflows/build_make.yml +++ b/.github/workflows/build_make.yml @@ -22,7 +22,7 @@ jobs: steps: # Checkout the code of the current branch - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 # Update apt-get database - name: Update apt-get database @@ -42,9 +42,9 @@ jobs: # Get an OCaml environment with opam installed and the proper ocaml version # opam will used opam cache environment if retrieved - name: Use OCaml ${{ env.OCAML_DEFAULT_VERSION }} - uses: avsm/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v2 with: - ocaml-version: ${{ env.OCAML_DEFAULT_VERSION }} + ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }} # Pin the packages, this is needed for opam depext # remove this step when opam 2.1 will be used @@ -94,7 +94,7 @@ jobs: steps: # Checkout the code of the current branch - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 # Update apt-get database - name: Update apt-get database @@ -114,9 +114,9 @@ jobs: # Get an OCaml environment with opam installed and the proper ocaml version # opam will used opam cache environment if retrieved - name: Use OCaml ${{ env.OCAML_DEFAULT_VERSION }} - uses: avsm/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v2 with: - ocaml-version: ${{ env.OCAML_DEFAULT_VERSION }} + ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }} # Pin the packages, this is needed for opam depext # remove this step when opam 2.1 will be used @@ -168,7 +168,7 @@ jobs: steps: # Checkout the code of the current branch - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 # Update apt-get database - name: Update apt-get database @@ -186,16 +186,16 @@ jobs: key: v1-${{ runner.os }}-alt-ergo-make-${{ matrix.package }}-${{ env.OCAML_DEFAULT_VERSION }}-${{ hashFiles('*.opam') }} - name: Use OCaml ${{ env.OCAML_DEFAULT_VERSION }} - uses: avsm/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v2 with: - ocaml-version: ${{ env.OCAML_DEFAULT_VERSION }} + ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }} # Get an OCaml environment with opam installed and the proper ocaml version # opam will used opam cache environment if retrieved - name: Use OCaml ${{ env.OCAML_DEFAULT_VERSION }} - uses: avsm/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v2 with: - ocaml-version: ${{ env.OCAML_DEFAULT_VERSION }} + ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }} # Pin the packages, this is needed for opam depext # remove this step when opam 2.1 will be used diff --git a/.github/workflows/build_ubuntu.yml b/.github/workflows/build_ubuntu.yml index 603ee6154..a4e132a0f 100644 --- a/.github/workflows/build_ubuntu.yml +++ b/.github/workflows/build_ubuntu.yml @@ -29,7 +29,7 @@ jobs: steps: # Checkout the code of the current branch - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 # Update apt-get database - name: Update apt-get database @@ -49,9 +49,9 @@ jobs: # Get an OCaml environment with opam installed and the proper ocaml version # opam will used opam cache environment if retrieved - name: Use OCaml ${{ env.OCAML_DEFAULT_VERSION }} - uses: avsm/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v2 with: - ocaml-version: ${{ env.OCAML_DEFAULT_VERSION }} + ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }} # Pin the packages, this is needed for opam depext # remove this step when opam 2.1 will be used @@ -107,7 +107,7 @@ jobs: strategy: matrix: # Setup ocaml versions to test - ocaml-version: + ocaml-compiler: - 4.05.0 - 4.05.0+flambda - 4.06.1 @@ -126,7 +126,7 @@ jobs: steps: # Checkout the code of the current branch - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 # Update apt-get database - name: Update apt-get database @@ -141,14 +141,14 @@ jobs: id: cache-opam with: path: ~/.opam - key: v1-${{ runner.os }}-alt-ergo-${{ matrix.ocaml-version }}-${{ hashFiles('*.opam') }} + key: v1-${{ runner.os }}-alt-ergo-${{ matrix.ocaml-compiler }}-${{ hashFiles('*.opam') }} # Get an OCaml environment with opam installed and the proper ocaml version # opam will used opam cache environment if retrieved - name: Use OCaml ${{ env.OCAML_DEFAULT_VERSION }} - uses: avsm/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v2 with: - ocaml-version: ${{ env.OCAML_DEFAULT_VERSION }} + ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }} # Pin the packages, this is needed for opam depext # remove this step when opam 2.1 will be used diff --git a/.github/workflows/build_windows.yml b/.github/workflows/build_windows.yml index 25efc1050..599417595 100644 --- a/.github/workflows/build_windows.yml +++ b/.github/workflows/build_windows.yml @@ -24,7 +24,7 @@ jobs: steps: # Checkout the code of the current branch - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 # Retrieve the opam cache with unique key # A new cache is created/used if the `.opam` files changes or @@ -40,9 +40,9 @@ jobs: # Get an OCaml environment with opam installed and the proper ocaml version # opam will used opam cache environment if retrieved - name: Use OCaml ${{ env.OCAML_DEFAULT_VERSION }} - uses: avsm/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v2 with: - ocaml-version: ${{ env.OCAML_DEFAULT_VERSION }} + ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }} # Pin the packages, this is needed for opam depext # remove this step when opam 2.1 will be used diff --git a/.github/workflows/documentation.yml b/.github/workflows/documentation.yml index 74f73f067..57ce0fcdf 100644 --- a/.github/workflows/documentation.yml +++ b/.github/workflows/documentation.yml @@ -32,7 +32,7 @@ jobs: steps: # Checkout the code of the current branch - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 # Update apt-get database - name: Update apt-get database @@ -52,9 +52,9 @@ jobs: # Get an OCaml environment with opam installed and the proper ocaml version # opam will used opam cache environment if retrieved - name: Use OCaml ${{ env.OCAML_DEFAULT_VERSION }} - uses: avsm/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v2 with: - ocaml-version: ${{ env.OCAML_DEFAULT_VERSION }} + ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }} # Pin the packages, this is needed for opam depext # remove this step when opam 2.1 will be used @@ -111,7 +111,7 @@ jobs: steps: # Checkout the code of the current branch - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 # Build the sphinx documentation # and automatically print any error or warning diff --git a/.github/workflows/linter.yml b/.github/workflows/linter.yml index 516c8a626..4fddf3b9f 100644 --- a/.github/workflows/linter.yml +++ b/.github/workflows/linter.yml @@ -25,7 +25,7 @@ jobs: steps: # Checkout the code of the current branch - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 # Retrieve the opam cache with unique key # A new cache is created/used if the `.opam` files changes or @@ -41,9 +41,9 @@ jobs: # Get an OCaml environment with opam installed and the proper ocaml version # opam will used opam cache environment if retrieved - name: Use OCaml ${{ env.OCAML_DEFAULT_VERSION }} - uses: avsm/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v2 with: - ocaml-version: ${{ env.OCAML_DEFAULT_VERSION }} + ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }} # Install ocp-indent with the fixed version # Do nothing if ocp-indent is already installed @@ -65,7 +65,7 @@ jobs: steps: # Checkout the code of the current branch - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 # Retrieve the opam cache with unique key # A new cache is created/used if the `.opam` files changes or @@ -81,9 +81,9 @@ jobs: # Get an OCaml environment with opam installed and the proper ocaml version # opam will used opam cache environment if retrieved - name: Use OCaml ${{ env.OCAML_DEFAULT_VERSION }} - uses: avsm/setup-ocaml@v2 + uses: ocaml/setup-ocaml@v2 with: - ocaml-version: ${{ env.OCAML_DEFAULT_VERSION }} + ocaml-compiler: ${{ env.OCAML_DEFAULT_VERSION }} # Install dependencies of the ocpchecker executable # Dune and stdlib-shims is needed to build the executable diff --git a/Makefile b/Makefile index 336debe69..3759fbd14 100644 --- a/Makefile +++ b/Makefile @@ -116,6 +116,9 @@ AB-Why3: ln -sf $(INSTALL_DIR)/default/share/alt-ergo/plugins/AB-Why3-plugin.cma AB-Why3-plugin.cma ln -sf $(INSTALL_DIR)/default/share/alt-ergo/plugins/AB-Why3-plugin.cmxs AB-Why3-plugin.cmxs +js: gen + $(DUNE) build $(DUNE_FLAGS) @$(BJS_DIR)/all + # Build all plugins plugins: $(DUNE) build $(DUNE_FLAGS) \ diff --git a/alt-ergo-js.opam b/alt-ergo-js.opam new file mode 100644 index 000000000..e7d8578c3 --- /dev/null +++ b/alt-ergo-js.opam @@ -0,0 +1,41 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +version: "2.4.3" +synopsis: "The Alt-Ergo SMT prover" +description: """ +Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro. + +See more details on https://alt-ergo.ocamlpro.com/""" +maintainer: ["Alt-Ergo developers"] +authors: ["Alt-Ergo developers"] +homepage: "https://alt-ergo.ocamlpro.com/" +doc: "https://ocamlpro.github.io/alt-ergo" +bug-reports: "https://github.com/OCamlPro/alt-ergo/issues" +depends: [ + "dune" {>= "2.8"} + "ocaml" {>= "4.05.0"} + "alt-ergo-lib" {= version} + "alt-ergo-parsers" {= version} + "js_of_ocaml" {>= "4.0.1" & <= "5.0.1"} + "js_of_ocaml-lwt" + "js_of_ocaml-ppx" + "data-encoding" + "zarith_stubs_js" + "lwt_ppx" + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git" diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam index c3b2cf427..bb2138fe6 100644 --- a/alt-ergo-lib.opam +++ b/alt-ergo-lib.opam @@ -14,8 +14,8 @@ homepage: "https://alt-ergo.ocamlpro.com/" doc: "https://ocamlpro.github.io/alt-ergo" bug-reports: "https://github.com/OCamlPro/alt-ergo/issues" depends: [ + "dune" {>= "2.8"} "ocaml" {>= "4.05.0"} - "dune" {>= "2.0"} "dune-configurator" "dune-build-info" "num" diff --git a/alt-ergo-parsers.opam b/alt-ergo-parsers.opam index 756d5a49c..6dd60fbd0 100644 --- a/alt-ergo-parsers.opam +++ b/alt-ergo-parsers.opam @@ -14,8 +14,8 @@ homepage: "https://alt-ergo.ocamlpro.com/" doc: "https://ocamlpro.github.io/alt-ergo" bug-reports: "https://github.com/OCamlPro/alt-ergo/issues" depends: [ + "dune" {>= "2.8"} "ocaml" {>= "4.05.0"} - "dune" {>= "2.0"} "alt-ergo-lib" {= version} "psmt2-frontend" {>= "0.3"} "camlzip" {>= "1.07"} diff --git a/alt-ergo.opam b/alt-ergo.opam index 642384586..18f72689d 100644 --- a/alt-ergo.opam +++ b/alt-ergo.opam @@ -12,8 +12,8 @@ homepage: "https://alt-ergo.ocamlpro.com/" doc: "https://ocamlpro.github.io/alt-ergo" bug-reports: "https://github.com/OCamlPro/alt-ergo/issues" depends: [ + "dune" {>= "2.8"} "ocaml" {>= "4.05.0"} - "dune" {>= "2.0"} "alt-ergo-lib" {= version} "alt-ergo-parsers" {= version} "menhir" diff --git a/altgr-ergo.opam b/altgr-ergo.opam index 24b95da40..93c4270b0 100644 --- a/altgr-ergo.opam +++ b/altgr-ergo.opam @@ -14,8 +14,8 @@ homepage: "https://alt-ergo.ocamlpro.com/" doc: "https://ocamlpro.github.io/alt-ergo" bug-reports: "https://github.com/OCamlPro/alt-ergo/issues" depends: [ + "dune" {>= "2.8"} "ocaml" {>= "4.05.0"} - "dune" {>= "2.0"} "alt-ergo-lib" {= version} "alt-ergo-parsers" {= version} "lablgtk3" diff --git a/dune-project b/dune-project index 9bd212a64..b9b58f34d 100644 --- a/dune-project +++ b/dune-project @@ -1,5 +1,4 @@ -(lang dune 2.0) -(allow_approximate_merlin) +(lang dune 2.8) ; Since we want to generate opam files we need to provide informations ; (generate_opam_files true) @@ -26,13 +25,32 @@ Alt-Ergo is an automatic theorem prover of mathematical formulas. It was develop See more details on https://alt-ergo.ocamlpro.com/") (depends (ocaml (>= 4.05.0)) - (dune (and (>= 2.0))) (alt-ergo-lib (= :version)) (alt-ergo-parsers (= :version)) menhir (cmdliner (>= 1.1.0)) (odoc :with-doc) - ) + ) +) + +(package + (name alt-ergo-js) + (synopsis "The Alt-Ergo SMT prover") + (description "\ +Alt-Ergo is an automatic theorem prover of mathematical formulas. It was developed at LRI, and is now maintained at OCamlPro. + +See more details on https://alt-ergo.ocamlpro.com/") + (depends + (ocaml (>= 4.05.0)) + (alt-ergo-lib (= :version)) + (alt-ergo-parsers (= :version)) + (js_of_ocaml (and (>= 4.0.1) (<= 5.0.1))) + js_of_ocaml-lwt + js_of_ocaml-ppx + data-encoding + zarith_stubs_js + lwt_ppx + ) ) ; Second package, the alt-ergo gui binary @@ -51,7 +69,6 @@ See more details on https://alt-ergo.ocamlpro.com/" (depends (ocaml (>= 4.05.0)) - (dune (and (>= 2.0))) (alt-ergo-lib (= :version)) (alt-ergo-parsers (= :version)) lablgtk3 @@ -59,7 +76,7 @@ See more details on https://alt-ergo.ocamlpro.com/" lablgtk3-sourceview3 (cmdliner (>= 1.1.0)) (odoc :with-doc) -) + ) ) ; Third package, the alt-ergo parsers library @@ -78,7 +95,6 @@ See more details on http://alt-ergo.ocamlpro.com/" (depends (ocaml (>= 4.05.0)) - (dune (and (>= 2.0))) (alt-ergo-lib (= :version)) (psmt2-frontend (>= 0.3)) (camlzip (>= 1.07)) @@ -104,7 +120,6 @@ See more details on http://alt-ergo.ocamlpro.com/" (depends (ocaml (>= 4.05.0)) - (dune (and (>= 2.0))) dune-configurator dune-build-info num diff --git a/src/bin/js/dune b/src/bin/js/dune index 8a9c2dc2d..56032865e 100644 --- a/src/bin/js/dune +++ b/src/bin/js/dune @@ -1,39 +1,52 @@ ; Rule to build a js version runnable with node-js of Alt-Ergo (executable - (name main_text_js) - (libraries alt_ergo_common zarith_stubs_js) - (modules main_text_js) - (modes byte js) - (js_of_ocaml - (flags --no-source-map) - ) + (name main_text_js) + (public_name alt-ergo-js) + (package alt-ergo-js) + (libraries + alt_ergo_common + zarith_stubs_js + ) + (modules main_text_js) + (modes byte js) + (js_of_ocaml (flags --no-source-map +toplevel.js +dynlink.js)) ) (library - (name worker_interface) - (libraries js_of_ocaml data-encoding) - (modules worker_interface) + (name worker_interface) + (package alt-ergo-js) + (libraries + js_of_ocaml + data-encoding + ) + (modules worker_interface) ) ; Rule to build a web worker running Alt-Ergo (executable - (name worker_js) - (libraries worker_interface alt_ergo_common zarith_stubs_js js_of_ocaml js_of_ocaml-lwt) - (modules worker_js options_interface) - (modes byte js) - (js_of_ocaml - (flags --no-source-map) - ) + (name worker_js) + (libraries + worker_interface + alt_ergo_common + zarith_stubs_js + js_of_ocaml + js_of_ocaml-lwt + ) + (modules worker_js options_interface) + (modes byte js) + (js_of_ocaml (flags --no-source-map +toplevel.js +dynlink.js)) ) ; Rule to build a small js example running the Alt-Ergo web worker (executable - (name worker_example) - (libraries worker_interface zarith_stubs_js js_of_ocaml js_of_ocaml-lwt) - (modules worker_example) - (modes byte js) - (preprocess (pps js_of_ocaml-ppx lwt_ppx)) - (js_of_ocaml - (flags --no-source-map) - ) + (name worker_example) + (libraries + worker_interface + zarith_stubs_js + js_of_ocaml + js_of_ocaml-lwt + ) + (modules worker_example) + (modes byte js) + (preprocess (pps js_of_ocaml-ppx lwt_ppx)) ) diff --git a/src/dune b/src/dune index b9b3711ee..60b3359da 100644 --- a/src/dune +++ b/src/dune @@ -11,4 +11,5 @@ (flags (:standard -bin-annot)) (ocamlopt_flags -O3 -unbox-closures)) + (js_of_ocaml (flags --no-source-map)) ) diff --git a/src/lib/missing_primitives.js b/src/lib/missing_primitives.js index 9557e1304..b094022cc 100644 --- a/src/lib/missing_primitives.js +++ b/src/lib/missing_primitives.js @@ -2,12 +2,22 @@ // the missing primitives are replace with dummies //Provides: unix_times -//Requires: unix_gettimeofday +//Requires: caml_unix_gettimeofday function unix_times () { - var utime = unix_gettimeofday (); + var utime = caml_unix_gettimeofday (); return BLOCK(0, utime, utime, utime, utime) } //Provides: unix_setitimer function unix_setitimer () { return BLOCK(0, 0, 0, 0) } + +//Provides: unix_getpid +function unix_getpid() { + return 0; +} + +//Provides: unix_kill +function unix_kill() { + return 0; +}