From 749b51f6618d0d7a7f48b66e781d6ecf017bc24a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Tue, 16 Dec 2025 00:59:17 -0800
Subject: [PATCH 1/3] fstar.2025.12.15

Just a new F* release. For this release, we are switching the source
tarball to be a "source package" containing the OCaml-extracted sources
of F*, avoiding the need to bootstrap the compiler when installing via
OPAM.
---
 packages/fstar/fstar.2025.12.15/opam | 52 ++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 packages/fstar/fstar.2025.12.15/opam

diff --git a/packages/fstar/fstar.2025.12.15/opam b/packages/fstar/fstar.2025.12.15/opam
new file mode 100644
index 000000000000..cc7f1fda5b96
--- /dev/null
+++ b/packages/fstar/fstar.2025.12.15/opam
@@ -0,0 +1,52 @@
+opam-version: "2.0"
+maintainer: "mtzguido@gmail.com"
+authors: [
+  "Nik Swamy <nswamy@microsoft.com>"
+  "Jonathan Protzenko <protz@microsoft.com>"
+  "Tahina Ramananandro <taramana@microsoft.com>"
+]
+homepage: "http://fstar-lang.org"
+license: "Apache-2.0"
+depends: [
+  "ocaml" {>= "4.14.0"}
+  "batteries"
+  "zarith" {>= "1.14"}
+  "stdint"
+  "yojson"
+  "dune" { >= "3.8.0"}
+  "memtrace" {>= "0.2.3"}
+  "menhirLib"
+  "menhir" {build & >= "20230415"}
+  "mtime" {>= "2.1.0"}
+  "pprint"
+  "sedlex" {>= "3.5" }
+  "ppxlib" {>= "0.36.0" }
+  "process"
+  "ppx_deriving" {build}
+  "ppx_deriving_yojson" {build}
+]
+depexts: ["coreutils"] {os = "macos" & os-distribution = "homebrew"}
+build: [
+  [make "-j" jobs "ADMIT=1"]
+]
+install: [
+  [make "PREFIX=%{prefix}%" "install"]
+]
+post-messages: [
+  """
+F* requires specific versions of Z3 to work correctly, and will refuse to run
+if the version string does not match. You should have z3-4.8.5 and z3-4.13.3
+in your $PATH. For details, see
+https://github.com/FStarLang/FStar/blob/master/INSTALL.md#runtime-dependency-particular-version-of-z3.
+""" {success}
+]
+dev-repo: "git+https://github.com/FStarLang/FStar"
+bug-reports: "https://github.com/FStarLang/FStar/issues"
+synopsis: "Verification system for effectful programs"
+url {
+  src: "https://github.com/FStarLang/FStar/releases/download/v2025.12.15/fstar-v2025.12.15-src.tar.gz"
+  checksum: [
+    "md5=581ea8f957ee6c36662b0d4b62463a9a"
+    "sha512=6e548ed0656940ca7730ee08b192610f17a5ff0126dc5cabb32a7dcfe4bced06228b9e26ef785d12f141a4543a5cd8eb829c6aa5b02cbf1bdf04f200a7f57eac"
+  ]
+}

From 04d2f86ea398fda1f63fba7bbb75272dad5eec9d Mon Sep 17 00:00:00 2001
From: Shon Feder <shon.feder@gmail.com>
Date: Fri, 16 Jan 2026 21:42:01 -0500
Subject: [PATCH 2/3] Add upper bounds on ocaml 5.4 and dune

Add upper

Co-authored-by: Jan Midtgaard <mail@janmidtgaard.dk>
---
 packages/fstar/fstar.2025.12.15/opam | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/packages/fstar/fstar.2025.12.15/opam b/packages/fstar/fstar.2025.12.15/opam
index cc7f1fda5b96..021228af08e7 100644
--- a/packages/fstar/fstar.2025.12.15/opam
+++ b/packages/fstar/fstar.2025.12.15/opam
@@ -8,12 +8,12 @@ authors: [
 homepage: "http://fstar-lang.org"
 license: "Apache-2.0"
 depends: [
-  "ocaml" {>= "4.14.0"}
+  "ocaml" {>= "4.14.0" & < "5.4"}
   "batteries"
   "zarith" {>= "1.14"}
   "stdint"
   "yojson"
-  "dune" { >= "3.8.0"}
+  "dune" { >= "3.15.0"}
   "memtrace" {>= "0.2.3"}
   "menhirLib"
   "menhir" {build & >= "20230415"}

From 18add44372814950f963cf6119e6c41eb67598ae Mon Sep 17 00:00:00 2001
From: Marcello Seri <mseri@users.noreply.github.com>
Date: Fri, 23 Jan 2026 16:08:05 +0100
Subject: [PATCH 3/3] Apply suggestion

---
 packages/fstar/fstar.2025.12.15/opam | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/packages/fstar/fstar.2025.12.15/opam b/packages/fstar/fstar.2025.12.15/opam
index 021228af08e7..7f00e4a38e25 100644
--- a/packages/fstar/fstar.2025.12.15/opam
+++ b/packages/fstar/fstar.2025.12.15/opam
@@ -13,7 +13,7 @@ depends: [
   "zarith" {>= "1.14"}
   "stdint"
   "yojson"
-  "dune" { >= "3.15.0"}
+  "dune" { >= "3.16.0"}
   "memtrace" {>= "0.2.3"}
   "menhirLib"
   "menhir" {build & >= "20230415"}