public inbox for git-commits@fedoraproject.org
help / color / mirror / Atom feed
From: Jerry James <loganjerry@gmail.com>
To: git-commits@fedoraproject.org
Subject: [rpms/gappalib-coq] rawhide: Rebuild for rocq 9.3.0
Date: Sun, 27 Sep 2026 04:03:04 GMT [thread overview]
Message-ID: <179048178426.1.14760934667998831106.rpms-gappalib-coq-a42cb3ffe46d@fedoraproject.org> (raw)
A new commit has been pushed.
Repo : rpms/gappalib-coq
Branch : rawhide
Commit : a42cb3ffe46d7bde1d2ed106ca4b35b9d02a8f92
Author : Jerry James <loganjerry@gmail.com>
Date : 2026-09-26T22:02:52-06:00
Stats : +84/-2 in 2 file(s)
URL : https://src.fedoraproject.org/rpms/gappalib-coq/c/a42cb3ffe46d7bde1d2ed106ca4b35b9d02a8f92?branch=rawhide
Log:
Rebuild for rocq 9.3.0
---
diff --git a/gappalib-coq-rocq9.3.patch b/gappalib-coq-rocq9.3.patch
new file mode 100644
index 0000000..6de3fe9
--- /dev/null
+++ b/gappalib-coq-rocq9.3.patch
@@ -0,0 +1,80 @@
+--- gappalib-coq-1.11.0/configure.in.orig 2026-06-01 03:15:04.000000000 -0600
++++ gappalib-coq-1.11.0/configure.in 2026-09-26 20:04:58.697886008 -0600
+@@ -50,7 +50,7 @@ AC_MSG_CHECKING([for Flocq >= 4.1])
+ AS_IF(
+ [ echo "From Flocq Require Import Version." \
+ "From Coq Require Import BinNat." \
+- "Goal (40100 <= Flocq_version)%N. easy. Qed." > conftest.v
++ "Goal (40100 <= Flocq_version)%N. Proof. easy. Qed." > conftest.v
+ $COQC conftest.v > conftest.err ],
+ [ AC_MSG_RESULT([yes]) ],
+ [ AC_MSG_RESULT([no])
+@@ -85,7 +85,7 @@ if test "$native_tactic" = yes; then
+ AC_MSG_CHECKING([for native development files])
+ AS_IF(
+ [ echo "let _ = (Evd.empty, Big_int_Z.zero_big_int)" > conftest.ml
+- $OCAMLFIND ocamlopt -rectypes -thread -package coq-core.engine -package zarith -shared conftest.ml -o conftest.cmxs ],
++ $OCAMLFIND ocamlopt -rectypes -thread -package rocq-runtime.engine -package zarith -shared conftest.ml -o conftest.cmxs ],
+ [ AC_MSG_RESULT(yes) ],
+ [ AC_MSG_RESULT(no)
+ AC_MSG_ERROR([ *** Failed to compile a native OCaml library ]) ])
+@@ -95,7 +95,7 @@ if test "$byte_tactic" = yes; then
+ AC_MSG_CHECKING([for bytecode development files])
+ AS_IF(
+ [ echo "let _ = (Evd.empty, Big_int_Z.zero_big_int)" > conftest.ml
+- $OCAMLFIND ocamlc -rectypes -thread -package coq-core.engine -package zarith -c conftest.ml -o conftest.cmo ],
++ $OCAMLFIND ocamlc -rectypes -thread -package rocq-runtime.engine -package zarith -c conftest.ml -o conftest.cmo ],
+ [ AC_MSG_RESULT(yes) ],
+ [ AC_MSG_RESULT(no)
+ AC_MSG_ERROR([ *** Failed to compile a bytecode OCaml library ]) ])
+--- gappalib-coq-1.11.0/configure.orig 2026-06-01 03:15:04.000000000 -0600
++++ gappalib-coq-1.11.0/configure 2026-09-26 20:05:40.601417452 -0600
+@@ -3685,7 +3685,7 @@ printf "%s\n" "$OCAMLLEX" >&6; }
+ printf %s "checking for Flocq >= 4.1... " >&6; }
+ if echo "From Flocq Require Import Version." \
+ "From Coq Require Import BinNat." \
+- "Goal (40100 <= Flocq_version)%N. easy. Qed." > conftest.v
++ "Goal (40100 <= Flocq_version)%N. Proof. easy. Qed." > conftest.v
+ $COQC conftest.v > conftest.err
+ then :
+ { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5
+@@ -3734,7 +3734,7 @@ if test "$native_tactic" = yes; then
+ { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for native development files" >&5
+ printf %s "checking for native development files... " >&6; }
+ if echo "let _ = (Evd.empty, Big_int_Z.zero_big_int)" > conftest.ml
+- $OCAMLFIND ocamlopt -rectypes -thread -package coq-core.engine -package zarith -shared conftest.ml -o conftest.cmxs
++ $OCAMLFIND ocamlopt -rectypes -thread -package rocq-runtime.engine -package zarith -shared conftest.ml -o conftest.cmxs
+ then :
+ { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5
+ printf "%s\n" "yes" >&6; }
+@@ -3749,7 +3749,7 @@ if test "$byte_tactic" = yes; then
+ { printf "%s\n" "$as_me:${as_lineno-$LINENO}: checking for bytecode development files" >&5
+ printf %s "checking for bytecode development files... " >&6; }
+ if echo "let _ = (Evd.empty, Big_int_Z.zero_big_int)" > conftest.ml
+- $OCAMLFIND ocamlc -rectypes -thread -package coq-core.engine -package zarith -c conftest.ml -o conftest.cmo
++ $OCAMLFIND ocamlc -rectypes -thread -package rocq-runtime.engine -package zarith -c conftest.ml -o conftest.cmo
+ then :
+ { printf "%s\n" "$as_me:${as_lineno-$LINENO}: result: yes" >&5
+ printf "%s\n" "yes" >&6; }
+--- gappalib-coq-1.11.0/Remakefile.in.orig 2026-06-01 03:15:04.000000000 -0600
++++ gappalib-coq-1.11.0/Remakefile.in 2026-09-26 20:04:11.793997256 -0600
+@@ -50,7 +50,7 @@ tools/vdep.exe: tools/vdep.ml
+ @COQC@ @COQEXTRAFLAGS@ -q -R src Gappa -I src $<
+
+ COQPKGS = clib engine kernel interp lib library parsing pretyping printing proofs tactics toplevel vernac plugins.ltac
+-PACKAGES = $(addprefix -package coq-core., $(COQPKGS)) -package zarith
++PACKAGES = $(addprefix -package rocq-runtime., $(COQPKGS)) -package zarith
+
+ src/gappatac.ml: src/gappatac.c Remakefile
+ @CPP@ -DCOQVERSION=@COQVERSION@ $< -o $@
+--- gappalib-coq-1.11.0/src/META.coq-gappa.orig 2026-06-01 03:15:04.000000000 -0600
++++ gappalib-coq-1.11.0/src/META.coq-gappa 2026-09-26 20:06:56.138208533 -0600
+@@ -1,7 +1,7 @@
+ package "tactic" (
+ directory = "."
+ description = "Coq Gappa"
+- requires = "coq-core.plugins.ltac"
++ requires = "rocq-runtime.plugins.ltac"
+ archive(byte) = "gappatac.cma"
+ archive(native) = "gappatac.cmxa"
+ plugin(byte) = "gappatac.cma"
diff --git a/gappalib-coq.spec b/gappalib-coq.spec
index c0fc137..480524d 100644
--- a/gappalib-coq.spec
+++ b/gappalib-coq.spec
@@ -3,7 +3,7 @@
# install the package and run "remake check" manually before committing.
%global gappadir %{ocamldir}/coq/user-contrib/Gappa
-%global rocqver 9.2.0
+%global rocqver 9.3.0
Name: gappalib-coq
Version: 1.11.0
@@ -14,6 +14,8 @@ License: LGPL-3.0-or-later
URL: https://gappa.gitlabpages.inria.fr/
VCS: git:https://gitlab.inria.fr/gappa/coq.git
Source: %{url}releases/%{name}-%{version}.tar.gz
+# Adapt to rocq 9.3
+Patch: %{name}-rocq9.3.patch
# Coq's plugin architecture requires cmxs files
ExclusiveArch: %{ocaml_native_compiler}
@@ -53,7 +55,7 @@ files are not needed to use gappalib-coq. They are made available for
informational purposes.
%prep
-%autosetup
+%autosetup -p1
%conf
# Enable debuginfo
reply other threads:[~2026-09-27 4:03 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=179048178426.1.14760934667998831106.rpms-gappalib-coq-a42cb3ffe46d@fedoraproject.org \
--to=loganjerry@gmail.com \
--cc=git-commits@fedoraproject.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox