Rebase 2.4.3 (#597)

* Fix zarith dependency (#592) * Require Zarith >= 1.4 * Disable warnings 22 in release profile also * Update documentation * Update changes * Increase the minimal version of Cairo 2 * Increase the minimal version of psmt2-frontend * Clarify licenses (#595) * Clarify licenses * Poetry * Finish release 2.4.3 (#581) * Add the changes log * Update the changes log * Active the windows CI on the branch 2.4.x * Refactoring the release target * Add headers for the licenses * Add the CeCILL license * Update the headers for 2023 * Fix spdx warning and add a template for the opam file of alt-ergo-js * Add the target for the free release * Fix the directory paths for licenses * Fix the issue with js_of_ocaml flags by using at least Dune 3.0 * Update opam files * Update headers for the new files * Remove the header in the script configure.ml
OCamlPro · May 16, 2023 · 1a06e2f · 1a06e2f
1 parent b8abf41
commit 1a06e2f
Show file tree

Hide file tree

Showing 221 changed files with 6,946 additions and 4,107 deletions.
diff --git a/.github/workflows/build_windows.yml b/.github/workflows/build_windows.yml
@@ -7,6 +7,7 @@ on:
       - fix-ci
       - next
       - main
+      - 2.4.x
 
 env:
   OCAML_DEFAULT_VERSION: 4.10.0

diff --git a/CHANGES.md b/CHANGES.md
@@ -0,0 +1,16 @@
+## v2.4.3 (2023-04-14)
+
+# Build
+* Restrict the requirement version of Ocplib-simplex (PR #573)
+* Dune 3.0 or above required, see https://github.com/ocaml/dune/issues/5563 (PR #575)
+* Zarith 1.4 or above required
+* Cairo2 0.6.4 or above required
+* psmt2-frontend 0.4 or above required
+* Using js_of_ocaml with a version between 4.0.1 and 5.0.1 required (PR #575)
+
+# Bug fixes
+* Fix soundness issues in the arithmetic reasoner #476, #477, #479 (PR #573)
+
+# Regression fixes
+* Remove flattening, see issues #505, #567 (PR #573)
+* Using a weak table for the Shostak.combine cache to prevent some regressions (PR #573)
diff --git a/Makefile b/Makefile
@@ -291,23 +291,47 @@ VERSION_NUM=$(VERSION:v%=%)
 # Some convenient variables
 PUBLIC_RELEASE=alt-ergo-$(VERSION_NUM)
 PUBLIC_TARGZ=$(PUBLIC_RELEASE).tar.gz
-FILES_DEST=public-release/$(PUBLIC_RELEASE)/$(PUBLIC_RELEASE)
+FILES_DEST=public-release/$(PUBLIC_RELEASE)
 
-public-release:
-	rm -rf public-release
+--prepare-release:
+	git clean -dfxi
 	mkdir -p $(FILES_DEST)
-	cp configure configure.ml *.opam dune-project dune $(FILES_DEST)
-	git clean -dfx
-	cp licenses/License.OCamlPro licences/OCamlPro-Non-Commercial-License.txt licenses/OCamlPro-Non-Commercial-License.pdf licenses/LGPL-License.txt licenses/Apache-License-2.0.txt $(FILES_DEST)/
-	cp README.md LICENSE.md COPYING.md $(FILES_DEST)/
-	cp Makefile $(FILES_DEST)/
-	cp INSTALL.md alt-ergo.opam CHANGES $(FILES_DEST)/
-	cp -rf lib bin common parsers preludes examples doc $(FILES_DEST)/
-	cp -rf plugins $(FILES_DEST)/ 2> /dev/null || echo "cp: skip plugins dir (not found)"
+	cp --parents -r \
+	docs \
+	examples \
+	licenses/Apache-License-2.0.txt \
+	licenses/OCamlPro-Non-Commercial-License.pdf \
+	licenses/OCamlPro-Non-Commercial-License.txt \
+	licenses/LGPL-License.txt \
+	non-regression \
+	rsc \
+	src \
+	tests \
+	configure \
+	configure.ml \
+	alt-ergo.opam \
+	alt-ergo-lib.opam \
+	alt-ergo-parsers.opam \
+	altgr-ergo.opam \
+	dune-project \
+	Makefile \
+	README.md \
+	LICENSE.md \
+	CHANGES.md \
+	$(FILES_DEST)
 	sed -i "s/%%VERSION_NUM%%/$(VERSION_NUM)/" $(FILES_DEST)/$(UTIL_DIR)/version.ml
 	sed -i "s/%%VCS_COMMIT_ID%%/$(VCS_COMMIT_ID)/" $(FILES_DEST)/$(UTIL_DIR)/version.ml
 	sed -i "s/%%BUILD_DATE%%/`LANG=en_US; date`/" $(FILES_DEST)/$(UTIL_DIR)/version.ml
-	cd $(FILES_DEST)/.. && tar cfz $(PUBLIC_TARGZ) $(PUBLIC_RELEASE)
+
+public-release: --prepare-release
+	cd public-release && tar cfz $(PUBLIC_TARGZ) $(PUBLIC_RELEASE)
+	rm -rf $(FILES_DEST)
+
+free-public-release: --prepare-release
+	cp licenses/CeCILL-C-License-v1.txt $(FILES_DEST)
+	find src/lib src/bin src/parsers -iname "*.ml*" -exec headache -h licenses/free-header.txt {} \;
+	cd public-release && tar cfz $(PUBLIC_TARGZ) $(PUBLIC_RELEASE)
+	git restore $(SRC_DIR)
 	rm -rf $(FILES_DEST)
 
 # ==============

diff --git a/alt-ergo-js.opam.template b/alt-ergo-js.opam.template
@@ -0,0 +1,15 @@
+# This part comes from the template. Please edit alt-ergo-js.opam.template
+# and not alt-ergo-js.opam which is generated by dune
+tags: "org:OCamlPro"
+
+license: [
+  "LicenseRef-OCamlpro-Non-Commercial"
+  "Apache-2.0"
+  "LGPL-2.1-only"
+]
+
+build: [
+  ["ocaml" "unix.cma" "configure.ml" name "--prefix" prefix "--libdir" lib "--mandir" man]
+  ["dune" "subst"] {pinned}
+  ["dune" "build" "-p" name "-j" jobs]
+]
diff --git a/alt-ergo-lib.opam b/alt-ergo-lib.opam
@@ -22,19 +22,21 @@ depends: [
   "dolmen_loop" {>= "0.8.1"}
   "num"
   "ocplib-simplex" {>= "0.5"}
-  "zarith"
+  "zarith" {>= "1.4"}
   "seq"
   "stdlib-shims"
   "camlzip" {>= "1.07"}
   "odoc" {with-doc}
 ]
 dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
-# This part comes from the template. Please edit alt-ergo.opam.template
+# This part comes from the template. Please edit alt-ergo-lib.opam.template
 # and not alt-ergo-lib.opam which is generated by dune
 tags: "org:OCamlPro"
 
 license: [
-  "OCamlPro Non-Commercial Purpose License, version 1"
+  "LicenseRef-OCamlpro-Non-Commercial"
+  "Apache-2.0"
+  "LGPL-2.1-only"
 ]
 
 build: [

diff --git a/alt-ergo-lib.opam.template b/alt-ergo-lib.opam.template
@@ -1,9 +1,11 @@
-# This part comes from the template. Please edit alt-ergo.opam.template
+# This part comes from the template. Please edit alt-ergo-lib.opam.template
 # and not alt-ergo-lib.opam which is generated by dune
 tags: "org:OCamlPro"
 
 license: [
-  "OCamlPro Non-Commercial Purpose License, version 1"
+  "LicenseRef-OCamlpro-Non-Commercial"
+  "Apache-2.0"
+  "LGPL-2.1-only"
 ]
 
 build: [

diff --git a/alt-ergo-parsers.opam b/alt-ergo-parsers.opam
@@ -16,18 +16,20 @@ depends: [
   "ocaml" {>= "4.05.0"}
   "dune" {>= "3.0"}
   "alt-ergo-lib" {= version}
-  "psmt2-frontend" {>= "0.3"}
+  "psmt2-frontend" {>= "0.4"}
   "menhir"
   "stdlib-shims"
   "odoc" {with-doc}
 ]
 dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
-# This part comes from the template. Please edit alt-ergo.opam.template
+# This part comes from the template. Please edit alt-ergo-parsers.opam.template
 # and not alt-ergo-parsers.opam which is generated by dune
 tags: "org:OCamlPro"
 
 license: [
-  "OCamlPro Non-Commercial Purpose License, version 1"
+  "LicenseRef-OCamlpro-Non-Commercial"
+  "Apache-2.0"
+  "LGPL-2.1-only"
 ]
 
 build: [

diff --git a/alt-ergo-parsers.opam.template b/alt-ergo-parsers.opam.template
@@ -1,9 +1,11 @@
-# This part comes from the template. Please edit alt-ergo.opam.template
+# This part comes from the template. Please edit alt-ergo-parsers.opam.template
 # and not alt-ergo-parsers.opam which is generated by dune
 tags: "org:OCamlPro"
 
 license: [
-  "OCamlPro Non-Commercial Purpose License, version 1"
+  "LicenseRef-OCamlpro-Non-Commercial"
+  "Apache-2.0"
+  "LGPL-2.1-only"
 ]
 
 build: [

diff --git a/alt-ergo.opam b/alt-ergo.opam
@@ -25,7 +25,8 @@ dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
 tags: "org:OCamlPro"
 
 license: [
-  "OCamlPro Non-Commercial Purpose License, version 1"
+  "LicenseRef-OCamlpro-Non-Commercial"
+  "Apache-2.0"
   "LGPL-2.1-only"
 ]
 

diff --git a/alt-ergo.opam.template b/alt-ergo.opam.template
@@ -3,7 +3,8 @@
 tags: "org:OCamlPro"
 
 license: [
-  "OCamlPro Non-Commercial Purpose License, version 1"
+  "LicenseRef-OCamlpro-Non-Commercial"
+  "Apache-2.0"
   "LGPL-2.1-only"
 ]
 

diff --git a/altgr-ergo.opam b/altgr-ergo.opam
@@ -18,18 +18,21 @@ depends: [
   "alt-ergo-lib" {= version}
   "alt-ergo-parsers" {= version}
   "lablgtk3"
+  "cairo2" {>= "0.6.4"}
   "conf-gtksourceview3"
   "lablgtk3-sourceview3"
   "cmdliner" {>= "1.1.0"}
   "odoc" {with-doc}
 ]
 dev-repo: "git+https://github.com/OCamlPro/alt-ergo.git"
-# This part comes from the template. Please edit alt-ergo.opam.template
+# This part comes from the template. Please edit altgr-ergo.opam.template
 # and not altgr-ergo.opam which is generated by dune
 tags: "org:OCamlPro"
 
 license: [
-  "OCamlPro Non-Commercial Purpose License, version 1"
+  "LicenseRef-OCamlpro-Non-Commercial"
+  "Apache-2.0"
+  "LGPL-2.1-only"
 ]
 
 build: [

diff --git a/altgr-ergo.opam.template b/altgr-ergo.opam.template
@@ -1,9 +1,11 @@
-# This part comes from the template. Please edit alt-ergo.opam.template
+# This part comes from the template. Please edit altgr-ergo.opam.template
 # and not altgr-ergo.opam which is generated by dune
 tags: "org:OCamlPro"
 
 license: [
-  "OCamlPro Non-Commercial Purpose License, version 1"
+  "LicenseRef-OCamlpro-Non-Commercial"
+  "Apache-2.0"
+  "LGPL-2.1-only"
 ]
 
 build: [
-Original file line number
+Diff line change
@@ Expand Up / @@ -7,6 +7,7 @@ on: @@
           - fix-ci
           - next
           - main
+          - 2.4.x
     env:
       OCAML_DEFAULT_VERSION: 4.10.0
@@ Expand Down @@