pkgsrc-Changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
CVS commit: pkgsrc/lang
Module Name: pkgsrc
Committed By: dkazankov
Date: Thu Jul 10 12:43:03 UTC 2025
Modified Files:
pkgsrc/lang: Makefile
Added Files:
pkgsrc/lang/spark2014-13: Makefile PLIST distinfo
pkgsrc/lang/spark2014-13/patches: patch-Makefile patch-gnatprove.gpr
patch-spark2014vsn.ads patch-src_common_platform.ads
patch-src_common_semaphores__c.c
patch-src_common_x86__64-netbsd_platform.adb
patch-src_gnatprove_spark__report.adb patch-why3_Makefile.in
Log Message:
lang/spark2014-13: Add new package version 13.3.0
SPARK 2014 toolset, FSF release 13.
A programming language, a verification toolset and a design method.
To generate a diff of this commit:
cvs rdiff -u -r1.762 -r1.763 pkgsrc/lang/Makefile
cvs rdiff -u -r0 -r1.1 pkgsrc/lang/spark2014-13/Makefile \
pkgsrc/lang/spark2014-13/PLIST pkgsrc/lang/spark2014-13/distinfo
cvs rdiff -u -r0 -r1.1 pkgsrc/lang/spark2014-13/patches/patch-Makefile \
pkgsrc/lang/spark2014-13/patches/patch-gnatprove.gpr \
pkgsrc/lang/spark2014-13/patches/patch-spark2014vsn.ads \
pkgsrc/lang/spark2014-13/patches/patch-src_common_platform.ads \
pkgsrc/lang/spark2014-13/patches/patch-src_common_semaphores__c.c \
pkgsrc/lang/spark2014-13/patches/patch-src_common_x86__64-netbsd_platform.adb \
pkgsrc/lang/spark2014-13/patches/patch-src_gnatprove_spark__report.adb \
pkgsrc/lang/spark2014-13/patches/patch-why3_Makefile.in
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
Modified files:
Index: pkgsrc/lang/Makefile
diff -u pkgsrc/lang/Makefile:1.762 pkgsrc/lang/Makefile:1.763
--- pkgsrc/lang/Makefile:1.762 Mon Jun 30 13:10:53 2025
+++ pkgsrc/lang/Makefile Thu Jul 10 12:43:03 2025
@@ -1,4 +1,4 @@
-# $NetBSD: Makefile,v 1.762 2025/06/30 13:10:53 ktnb Exp $
+# $NetBSD: Makefile,v 1.763 2025/07/10 12:43:03 dkazankov Exp $
#
COMMENT= Programming languages
@@ -334,6 +334,7 @@ SUBDIR+= smalltalk
SUBDIR+= smlnj
SUBDIR+= snobol
SUBDIR+= spago
+SUBDIR+= spark2014-13
SUBDIR+= spidermonkey
SUBDIR+= spidermonkey185
SUBDIR+= spl
Added files:
Index: pkgsrc/lang/spark2014-13/Makefile
diff -u /dev/null pkgsrc/lang/spark2014-13/Makefile:1.1
--- /dev/null Thu Jul 10 12:43:03 2025
+++ pkgsrc/lang/spark2014-13/Makefile Thu Jul 10 12:43:03 2025
@@ -0,0 +1,98 @@
+# $NetBSD: Makefile,v 1.1 2025/07/10 12:43:03 dkazankov Exp $
+
+DISTNAME= ${GITHUB_PROJECT}
+PKGNAME= ${GITHUB_PROJECT}-13-13.3.0
+CATEGORIES= lang devel
+MASTER_SITES= ${MASTER_SITE_GITHUB:=AdaCore/}
+GITHUB_PROJECT= spark2014
+# latest fsf-13 branch commit
+GITHUB_TAG= 12db22e854defa9d1c993ef904af1e72330a68ca
+DISTFILES= ${DEFAULT_DISTFILES}
+
+MAINTAINER= dkazankov%NetBSD.org@localhost
+HOMEPAGE= https://github.com/AdaCore/spark2014
+COMMENT= SPARK 2014 toolset, FSF release 13
+LICENSE= gnu-gpl-v3
+
+USE_LANGUAGES= c ada
+# GNAT major release must match SPARK2014 major release
+GCC_REQD+= 13
+
+USE_TOOLS+= gmake
+
+HAS_CONFIGURE= yes
+
+MKPIE_SUPPORTED= no
+RELRO_SUPPORTED= no
+
+GITHUB_SUBMODULES+= AdaCore alt-ergo be23b7992464438d6b654d9e36e6917748862130 alt-ergo
+GITHUB_SUBMODULES+= AdaCore cvc5 98b5fb70e8a94fd258bfc959c4a6fd0cc3537564 cvc5
+GITHUB_SUBMODULES+= AdaCore why3 52b6a590ba9bfc64aa0d22b41715358f26124a1f why3
+GITHUB_SUBMODULES+= AdaCore z3 7e79f0deb7c9d43f7637113be5b99391f14fcc2e z3
+
+# Do not use GNAT 13.4 sources
+GCC_DISTNAME= gcc-${PKGVERSION_NOREV}
+GCC_EXTRACT_SUFFIX= .tar.xz
+GCC_DISTFILE= ${GCC_DISTNAME}${GCC_EXTRACT_SUFFIX}
+
+DISTFILES+= ${GCC_DISTFILE}
+SITES.${GCC_DISTFILE}= ${MASTER_SITE_GNU:=gcc/${GCC_DISTNAME}/}
+
+.include "../../mk/bsd.prefs.mk"
+
+CONFIG_SHELL= ${MAKE_PROGRAM}
+CONFIGURE_ARGS+= DESTDIR=${DESTDIR} PREFIX=${GNAT_PREFIX}
+CONFIGURE_SCRIPT= setup
+
+MAKE_FLAGS+= DESTDIR=${DESTDIR} PREFIX=${GNAT_PREFIX}
+
+INSTALL_TARGET= install-all
+
+SUBST_CLASSES+= interpreter
+SUBST_STAGE.interpreter= pre-configure
+SUBST_FILES.interpreter= benchmark_script/*
+SUBST_MESSAGE.interpreter= Fix interpreter in ${SUBST_FILES.interpreter}
+SUBST_SED.interpreter= -e 's,/bin/bash,/bin/sh,g'
+
+post-extract:
+# Link GNAT sources to main build tree
+ ${RUN} cd ${WRKDIR}/${GITHUB_PROJECT}-${GITHUB_TAG} \
+ && ${LN} -s ../../${GCC_DISTNAME}/gcc/ada gnat2why/gnat_src
+
+post-install:
+# Fix group write mode
+ cd ${DESTDIR}${PREFIX} && \
+ ${CHMOD} -R -P g-w ./*
+
+GENERATE_PLIST+= \
+ cd ${DESTDIR}${PREFIX} && \
+ ${FIND} ${GNAT_PKGBASE} \( -type f -or -type l \) -print | ${SORT};
+
+.include "../../devel/gprbuild/buildlink3.mk"
+
+.include "../../textproc/ada-xmlada-24/buildlink3.mk"
+.include "../../devel/ada-libgpr-24/buildlink3.mk"
+.include "../../devel/ada-gnatcoll-core-24/buildlink3.mk"
+
+.include "../../lang/python/tool.mk"
+
+BUILDLINK_DEPMETHOD.ocaml= build
+.include "../../lang/ocaml/ocaml.mk"
+BUILDLINK_DEPMETHOD.ocamlgraph= build
+.include "../../devel/ocamlgraph/buildlink3.mk"
+BUILDLINK_DEPMETHOD.menhir= build
+.include "../../devel/menhir/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml-zarith= build
+.include "../../math/ocaml-zarith/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml-zip= build
+.include "../../archivers/ocaml-zip/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml-ocplib-simplex= build
+.include "../../math/ocaml-ocplib-simplex/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml-num= build
+.include "../../math/ocaml-num/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml-yojson= build
+.include "../../devel/ocaml-yojson/buildlink3.mk"
+
+.include "../../mk/pthread.buildlink3.mk"
+
+.include "../../mk/bsd.pkg.mk"
Index: pkgsrc/lang/spark2014-13/PLIST
diff -u /dev/null pkgsrc/lang/spark2014-13/PLIST:1.1
--- /dev/null Thu Jul 10 12:43:03 2025
+++ pkgsrc/lang/spark2014-13/PLIST Thu Jul 10 12:43:03 2025
@@ -0,0 +1,610 @@
+@comment $NetBSD: PLIST,v 1.1 2025/07/10 12:43:03 dkazankov Exp $
+gcc13-gnat/bin/gnat2why
+gcc13-gnat/bin/gnatprove
+gcc13-gnat/bin/spark_memcached_wrapper
+gcc13-gnat/bin/spark_report
+gcc13-gnat/bin/spark_semaphore_wrapper
+gcc13-gnat/bin/target.atp
+gcc13-gnat/include/spark/spark-big_integers.ads
+gcc13-gnat/include/spark/spark-big_integers__light.adb
+gcc13-gnat/include/spark/spark-big_integers__light.ads
+gcc13-gnat/include/spark/spark-big_intervals.ads
+gcc13-gnat/include/spark/spark-big_intervals__light.ads
+gcc13-gnat/include/spark/spark-big_reals.ads
+gcc13-gnat/include/spark/spark-big_reals__light.adb
+gcc13-gnat/include/spark/spark-big_reals__light.ads
+gcc13-gnat/include/spark/spark-containers-formal-doubly_linked_lists.adb
+gcc13-gnat/include/spark/spark-containers-formal-doubly_linked_lists.ads
+gcc13-gnat/include/spark/spark-containers-formal-hashed_maps.adb
+gcc13-gnat/include/spark/spark-containers-formal-hashed_maps.ads
+gcc13-gnat/include/spark/spark-containers-formal-hashed_sets.adb
+gcc13-gnat/include/spark/spark-containers-formal-hashed_sets.ads
+gcc13-gnat/include/spark/spark-containers-formal-holders.adb
+gcc13-gnat/include/spark/spark-containers-formal-holders.ads
+gcc13-gnat/include/spark/spark-containers-formal-ordered_maps.adb
+gcc13-gnat/include/spark/spark-containers-formal-ordered_maps.ads
+gcc13-gnat/include/spark/spark-containers-formal-ordered_sets.adb
+gcc13-gnat/include/spark/spark-containers-formal-ordered_sets.ads
+gcc13-gnat/include/spark/spark-containers-formal-unbounded_doubly_linked_lists.adb
+gcc13-gnat/include/spark/spark-containers-formal-unbounded_doubly_linked_lists.ads
+gcc13-gnat/include/spark/spark-containers-formal-unbounded_hashed_maps.adb
+gcc13-gnat/include/spark/spark-containers-formal-unbounded_hashed_maps.ads
+gcc13-gnat/include/spark/spark-containers-formal-unbounded_hashed_sets.adb
+gcc13-gnat/include/spark/spark-containers-formal-unbounded_hashed_sets.ads
+gcc13-gnat/include/spark/spark-containers-formal-unbounded_ordered_maps.adb
+gcc13-gnat/include/spark/spark-containers-formal-unbounded_ordered_maps.ads
+gcc13-gnat/include/spark/spark-containers-formal-unbounded_ordered_sets.adb
+gcc13-gnat/include/spark/spark-containers-formal-unbounded_ordered_sets.ads
+gcc13-gnat/include/spark/spark-containers-formal-unbounded_vectors.adb
+gcc13-gnat/include/spark/spark-containers-formal-unbounded_vectors.ads
+gcc13-gnat/include/spark/spark-containers-formal-vectors.adb
+gcc13-gnat/include/spark/spark-containers-formal-vectors.ads
+gcc13-gnat/include/spark/spark-containers-formal.ads
+gcc13-gnat/include/spark/spark-containers-functional-base.adb
+gcc13-gnat/include/spark/spark-containers-functional-base.ads
+gcc13-gnat/include/spark/spark-containers-functional-infinite_sequences.adb
+gcc13-gnat/include/spark/spark-containers-functional-infinite_sequences.ads
+gcc13-gnat/include/spark/spark-containers-functional-infinite_sequences__light.adb
+gcc13-gnat/include/spark/spark-containers-functional-infinite_sequences__light.ads
+gcc13-gnat/include/spark/spark-containers-functional-maps.adb
+gcc13-gnat/include/spark/spark-containers-functional-maps.ads
+gcc13-gnat/include/spark/spark-containers-functional-maps__light.adb
+gcc13-gnat/include/spark/spark-containers-functional-maps__light.ads
+gcc13-gnat/include/spark/spark-containers-functional-multisets.adb
+gcc13-gnat/include/spark/spark-containers-functional-multisets.ads
+gcc13-gnat/include/spark/spark-containers-functional-multisets__light.adb
+gcc13-gnat/include/spark/spark-containers-functional-multisets__light.ads
+gcc13-gnat/include/spark/spark-containers-functional-sets.adb
+gcc13-gnat/include/spark/spark-containers-functional-sets.ads
+gcc13-gnat/include/spark/spark-containers-functional-sets__light.adb
+gcc13-gnat/include/spark/spark-containers-functional-sets__light.ads
+gcc13-gnat/include/spark/spark-containers-functional-vectors.adb
+gcc13-gnat/include/spark/spark-containers-functional-vectors.ads
+gcc13-gnat/include/spark/spark-containers-functional-vectors__light.adb
+gcc13-gnat/include/spark/spark-containers-functional-vectors__light.ads
+gcc13-gnat/include/spark/spark-containers-functional.ads
+gcc13-gnat/include/spark/spark-containers-parameter_checks.adb
+gcc13-gnat/include/spark/spark-containers-parameter_checks.ads
+gcc13-gnat/include/spark/spark-containers-stable_sorting.adb
+gcc13-gnat/include/spark/spark-containers-stable_sorting.ads
+gcc13-gnat/include/spark/spark-containers-types.ads
+gcc13-gnat/include/spark/spark-containers-types__light.ads
+gcc13-gnat/include/spark/spark-containers.ads
+gcc13-gnat/include/spark/spark-containers__exec.ads
+gcc13-gnat/include/spark/spark-conversions-float_conversions.ads
+gcc13-gnat/include/spark/spark-conversions-long_float_conversions.ads
+gcc13-gnat/include/spark/spark-conversions-long_integer_conversions.ads
+gcc13-gnat/include/spark/spark-conversions.ads
+gcc13-gnat/include/spark/spark-cut_operations.adb
+gcc13-gnat/include/spark/spark-cut_operations.ads
+gcc13-gnat/include/spark/spark-higher_order-fold.adb
+gcc13-gnat/include/spark/spark-higher_order-fold.ads
+gcc13-gnat/include/spark/spark-higher_order.adb
+gcc13-gnat/include/spark/spark-higher_order.ads
+gcc13-gnat/include/spark/spark-lemmas-arithmetic.adb
+gcc13-gnat/include/spark/spark-lemmas-arithmetic.ads
+gcc13-gnat/include/spark/spark-lemmas-constrained_array.adb
+gcc13-gnat/include/spark/spark-lemmas-constrained_array.ads
+gcc13-gnat/include/spark/spark-lemmas-fixed_point_arithmetic.adb
+gcc13-gnat/include/spark/spark-lemmas-fixed_point_arithmetic.ads
+gcc13-gnat/include/spark/spark-lemmas-float_arithmetic.ads
+gcc13-gnat/include/spark/spark-lemmas-float_base.ads
+gcc13-gnat/include/spark/spark-lemmas-floating_point_arithmetic.adb
+gcc13-gnat/include/spark/spark-lemmas-floating_point_arithmetic.ads
+gcc13-gnat/include/spark/spark-lemmas-integer_arithmetic.ads
+gcc13-gnat/include/spark/spark-lemmas-long_float_arithmetic.ads
+gcc13-gnat/include/spark/spark-lemmas-long_integer_arithmetic.ads
+gcc13-gnat/include/spark/spark-lemmas-mod32_arithmetic.ads
+gcc13-gnat/include/spark/spark-lemmas-mod64_arithmetic.ads
+gcc13-gnat/include/spark/spark-lemmas-mod_arithmetic.adb
+gcc13-gnat/include/spark/spark-lemmas-mod_arithmetic.ads
+gcc13-gnat/include/spark/spark-lemmas-unconstrained_array.adb
+gcc13-gnat/include/spark/spark-lemmas-unconstrained_array.ads
+gcc13-gnat/include/spark/spark-lemmas.ads
+gcc13-gnat/include/spark/spark-pointers-abstract_maps.ads
+gcc13-gnat/include/spark/spark-pointers-pointers_with_aliasing.adb
+gcc13-gnat/include/spark/spark-pointers-pointers_with_aliasing.ads
+gcc13-gnat/include/spark/spark-pointers-pointers_with_aliasing_separate_memory.adb
+gcc13-gnat/include/spark/spark-pointers-pointers_with_aliasing_separate_memory.ads
+gcc13-gnat/include/spark/spark-pointers.ads
+gcc13-gnat/include/spark/spark-tests-array_lemmas.adb
+gcc13-gnat/include/spark/spark-tests-array_lemmas.ads
+gcc13-gnat/include/spark/spark-tests.ads
+gcc13-gnat/include/spark/spark.ads
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_is_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_protect__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_protect__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_scale__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_scale__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_is_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_protect__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_protect__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_scale__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_scale__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__tests__array_lemmas__test_ufloat__lemma_transitive_order__pragargs__forall.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__tests__array_lemmas__test_ufloat__lemma_transitive_order__pragargs__forall.v
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__tests__array_lemmas__test_uint__lemma_transitive_order__pragargs__forall.ctx
+gcc13-gnat/lib/gnat/proof/Coq/Ada___ada___spark__tests__array_lemmas__test_uint__lemma_transitive_order__pragargs__forall.v
+gcc13-gnat/lib/gnat/proof/Coq/common/float32_div_common.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/float32_mul_common.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/float64_div_common.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/float64_mul_common.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/float_div_is_monotonic.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/float_div_right_negative_is_monotonic.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/float_mult_by_less_than_one.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/float_mult_is_monotonic.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/float_mult_right_negative_is_monotonic.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_exp_monotonic.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_mod_symmetry.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_modular_div_is_monotonic.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_modular_div_then_mult_bounds_part1.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_modular_div_then_mult_bounds_part2.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_modular_mult_is_monotonic.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_modular_mult_is_strictly_monotonic.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_modular_mult_protect.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_modular_mult_scale.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_modular_mult_then_div_is_ident.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_modular_mult_then_mod_is_zero.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_mult_protect.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_raising_order_float.prf
+gcc13-gnat/lib/gnat/proof/Coq/common/lemma_raising_order_int.prf
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__is_float/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__is_float__2/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__is_integer/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__is_integer_32/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__is_integer_64/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_add_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_div_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_div_left_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_div_right_negative_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_integer_add_exact/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_integer_mul_exact/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_integer_sub_exact/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_mult_by_less_than_one/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_mult_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_mult_right_negative_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_rounding_error_add/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_rounding_error_div/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_rounding_error_mul/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_rounding_error_sub/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_sub_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_div_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_div_right_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_exp_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_exp_is_monotonic_2/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mod_range/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mod_symmetry/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mult_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mult_is_strictly_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mult_protect/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mult_scale/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mult_then_div_is_ident/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mult_then_mod_is_zero/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__is_float/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__is_float__2/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__is_integer/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__is_integer_32/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__is_integer_64/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_add_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_left_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_right_negative_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_integer_add_exact/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_integer_mul_exact/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_integer_sub_exact/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_by_less_than_one/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_right_negative_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_rounding_error_add/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_rounding_error_div/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_rounding_error_mul/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_rounding_error_sub/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_sub_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_div_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_div_right_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_exp_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_exp_is_monotonic_2/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mod_range/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mod_symmetry/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mult_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mult_is_strictly_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mult_protect/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mult_scale/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mult_then_div_is_ident/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mult_then_mod_is_zero/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_strictly_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_protect/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_scale/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_div_is_ident/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_mod_is_zero/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_strictly_monotonic/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_protect/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_scale/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_div_is_ident/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_mod_is_zero/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__tests__array_lemmas__test_transitive_order_float/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__tests__array_lemmas__test_transitive_order_float__2/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__tests__array_lemmas__test_transitive_order_int/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__tests__array_lemmas__test_transitive_order_int__2/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__tests__array_lemmas__test_ufloat__lemma_transitive_order/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___ada___spark__tests__array_lemmas__test_uint__lemma_transitive_order/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___spark__big_intervals__in_range/why3session.xml
+gcc13-gnat/lib/gnat/proof/sessions/ada___spark__big_intervals__next/why3session.xml
+gcc13-gnat/lib/gnat/sparklib.gpr
+gcc13-gnat/lib/gnat/sparklib_common.gpr
+gcc13-gnat/lib/gnat/sparklib_internal.gpr
+gcc13-gnat/lib/gnat/sparklib_light.gpr
+gcc13-gnat/libexec/spark/bin/fake_alt-ergo
+gcc13-gnat/libexec/spark/bin/fake_cvc4
+gcc13-gnat/libexec/spark/bin/fake_cvc5
+gcc13-gnat/libexec/spark/bin/fake_z3
+gcc13-gnat/libexec/spark/bin/gnat_server
+gcc13-gnat/libexec/spark/bin/gnatwhy3
+gcc13-gnat/libexec/spark/bin/gnatwhy3.hash
+gcc13-gnat/libexec/spark/bin/why3
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/bin/why3config.cmxs
+gcc13-gnat/libexec/spark/bin/why3cpulimit
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/bin/why3realize.cmxs
+gcc13-gnat/libexec/spark/bin/why3server
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/bin/why3session.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/commands/why3config.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/commands/why3doc.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/commands/why3execute.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/commands/why3extract.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/commands/why3pp.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/commands/why3prove.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/commands/why3realize.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/commands/why3replay.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/commands/why3session.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/commands/why3shell.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/commands/why3show.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/commands/why3wc.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/commands/why3webserver.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/plugins/ada_terms.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/plugins/cfg.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/plugins/dimacs.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/plugins/genequlin.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/plugins/gnat_json.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/plugins/microc.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/plugins/python.cmxs
+${PLIST.ocaml-opt}gcc13-gnat/libexec/spark/lib/why3/plugins/tptp.cmxs
+gcc13-gnat/libexec/spark/lib/why3/why3-call-pvs
+gcc13-gnat/libexec/spark/lib/why3/why3cpulimit
+gcc13-gnat/libexec/spark/lib/why3/why3server
+gcc13-gnat/libexec/spark/share/why3/drivers/alt-ergo_gnatprove.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/alt_ergo.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/alt_ergo_2_2_0.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/alt_ergo_2_3.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/alt_ergo_common.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/alt_ergo_fp.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/alt_ergo_model.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/alt_ergo_smt2.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/beagle.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/colibri.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/colibri2.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/coq-common.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/coq-realizations.aux
+gcc13-gnat/libexec/spark/share/why3/drivers/coq-realize.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/coq-ssreflect.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/coq.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/coq_gnatprove.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc3.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4-realize.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_14.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_15.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_15_counterexample.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_16.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_16.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_16_counterexample.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_17.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_17_counterexample.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_18_strings.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_18_strings_counterexample.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_bv.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_gnatprove.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_gnatprove_ce.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_gnatprove_extra_axioms.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_gnatprove_oldfloat.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc4_gnatprove_qf.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc5.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc5_counterexample.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc5_gnatprove.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/cvc5_gnatprove_ce.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/discrimination.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/eprover.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/gappa.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/iprover.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/isabelle-common.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/isabelle-realizations.aux
+gcc13-gnat/libexec/spark/share/why3/drivers/isabelle-realize.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/isabelle.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/mathematica.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/mathsat.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/metis.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/metitarski.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/no-bv.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/polypaver.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/princess.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/psyche.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/pvs-common.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/pvs-realizations.aux
+gcc13-gnat/libexec/spark/share/why3/drivers/pvs-realize.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/pvs.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/safeprover.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/simplify.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/smt-libv2-bv-realization.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/smt-libv2-bv.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/smt-libv2-floats-gnatprove.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/smt-libv2-floats-int_via_bv.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/smt-libv2-floats-int_via_real.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/smt-libv2-floats.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/smt-libv2-gnatprove.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/smt-libv2.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/smtlib-strings.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/spass.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/spass_types.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/tptp-tff0.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/tptp-tff1.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/tptp.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/vampire-smt.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/vampire.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/verit.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/why3.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/why3_smt.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/why3_tptp.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/yices-smt2.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/yices.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/z3.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/z3_432.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/z3_440.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/z3_440_counterexample.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/z3_471.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/z3_471_counterexample.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/z3_471_nobv.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/z3_bv.gen
+gcc13-gnat/libexec/spark/share/why3/drivers/z3_gnatprove.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/z3_gnatprove_ce.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/z3_no_quant.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/z3_smtv1.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/zenon.drv
+gcc13-gnat/libexec/spark/share/why3/drivers/zenon_modulo.drv
+gcc13-gnat/libexec/spark/share/why3/images/fatcow.rc
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/accept.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/bin.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/bomb.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/brick_delete.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/bullet_black.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/bullet_blue.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/bullet_green.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/bullet_red.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/bullet_white.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/cancel.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/control_pause_blue.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/control_play_blue.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/database_delete.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/ddr_memory.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/delete.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/exclamation.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/folder.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/help.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/magic_wand_2.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/multitool.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/package.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/pencil.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/readme-fatcow.txt
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/script.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/time_delete.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/timeline.png
+gcc13-gnat/libexec/spark/share/why3/images/fatcow/update.png
+gcc13-gnat/libexec/spark/share/why3/images/logo-why.png
+gcc13-gnat/libexec/spark/share/why3/lang/why3.lang
+gcc13-gnat/libexec/spark/share/why3/lang/why3c.lang
+gcc13-gnat/libexec/spark/share/why3/lang/why3py.lang
+gcc13-gnat/libexec/spark/share/why3/libs/coq/BuiltIn.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/HighOrd.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/SPARK.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/_CoqProject
+gcc13-gnat/libexec/spark/share/why3/libs/coq/bool/Bool.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/bv/BV_Gen.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/bv/Pow2int.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/floating_point/Double.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/floating_point/DoubleFormat.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/floating_point/GenFloat.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/floating_point/Rounding.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/floating_point/Single.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/floating_point/SingleFormat.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/for_drivers/ComputerOfEuclideanDivision.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/ieee_float/Float32.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/ieee_float/Float64.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/ieee_float/GenericFloat.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/ieee_float/RoundingMode.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/int/Abs.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/int/ComputerDivision.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/int/Div2.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/int/EuclideanDivision.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/int/Exponentiation.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/int/Int.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/int/MinMax.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/int/NumOf.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/int/Power.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/Append.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/Combine.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/Distinct.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/HdTl.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/HdTlNoOpt.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/Length.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/List.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/Mem.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/Nth.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/NthHdTl.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/NthLength.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/NthLengthAppend.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/NthNoOpt.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/NumOcc.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/Permut.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/RevAppend.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/list/Reverse.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/map/Const.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/map/Map.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/map/MapInjection.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/map/MapPermut.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/map/Occ.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/number/Coprime.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/number/Divisibility.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/number/Gcd.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/number/Parity.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/number/Prime.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/option/Option.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/real/Abs.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/real/ExpLog.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/real/FromInt.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/real/MinMax.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/real/PowerInt.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/real/PowerReal.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/real/Real.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/real/RealInfix.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/real/Square.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/real/Trigonometry.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/real/Truncate.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/set/Cardinal.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/set/Fset.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/set/FsetInduction.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/set/FsetInt.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/set/FsetSum.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/set/Set.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/set/SetApp.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/set/SetAppInt.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/set/SetImp.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/set/SetImpInt.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/spark/SPARK_Integer_Arithmetic.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/spark/SPARK_Raising_Order.v
+gcc13-gnat/libexec/spark/share/why3/libs/coq/version
+gcc13-gnat/libexec/spark/share/why3/libs/coq/version.in
+gcc13-gnat/libexec/spark/share/why3/provers-detection-data.conf
+gcc13-gnat/libexec/spark/share/why3/theories/algebra.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/array.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/bag.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/bintree.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/bool.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/bv.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/byte_string.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/cursor.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/debug.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/exn.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/floating_point.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/fmap.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/for_drivers.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/function.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/graph.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/hashtbl.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/ieee_float.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/int.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/io.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/list.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/mach/array.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/mach/bv.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/mach/c.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/mach/float.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/mach/fxp.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/mach/int.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/mach/matrix.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/mach/onetime.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/mach/peano.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/mach/tagset.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/map.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/matrix.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/microc.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/null.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/number.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/ocaml.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/option.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/pigeon.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/pqueue.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/python.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/queue.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/random.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/real.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/ref.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/regexp.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/relations.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/seq.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/set.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/stack.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/string.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/tptp.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/tree.mlw
+gcc13-gnat/libexec/spark/share/why3/theories/witness.mlw
+gcc13-gnat/libexec/spark/share/why3/why3session.dtd
+gcc13-gnat/share/spark/config/frames/config.xml
+gcc13-gnat/share/spark/config/generated_menus.json
+gcc13-gnat/share/spark/config/gnat2why/config.xml
+gcc13-gnat/share/spark/config/gnatprove.conf
+gcc13-gnat/share/spark/help.txt
+gcc13-gnat/share/spark/runtimes/README
+gcc13-gnat/share/spark/theories/_gnatprove_standard.mlw
+gcc13-gnat/share/spark/theories/_gnatprove_standard_th.why
+gcc13-gnat/share/spark/theories/ada__model.mlw
+gcc13-gnat/share/spark/theories/ada__model_th.why
Index: pkgsrc/lang/spark2014-13/distinfo
diff -u /dev/null pkgsrc/lang/spark2014-13/distinfo:1.1
--- /dev/null Thu Jul 10 12:43:03 2025
+++ pkgsrc/lang/spark2014-13/distinfo Thu Jul 10 12:43:03 2025
@@ -0,0 +1,28 @@
+$NetBSD: distinfo,v 1.1 2025/07/10 12:43:03 dkazankov Exp $
+
+BLAKE2s (AdaCore-alt-ergo-be23b7992464438d6b654d9e36e6917748862130.tar.gz) = f42986ecfb007c601538c5963e906714c9ce31fea1698e0d76330d47c594dd3b
+SHA512 (AdaCore-alt-ergo-be23b7992464438d6b654d9e36e6917748862130.tar.gz) =
2776cfedf13e91b93fcb0b9f6c531a179438b2920908e662f008ca81f705811a52c3350c4c9b239639ee965ff9e3d9ec0fdf3967cc68f3f555cc1c2125d4c49d
+Size (AdaCore-alt-ergo-be23b7992464438d6b654d9e36e6917748862130.tar.gz) = 2883794 bytes
+BLAKE2s (AdaCore-cvc5-98b5fb70e8a94fd258bfc959c4a6fd0cc3537564.tar.gz) = e464cbc74aabd853d276543cbdadd741b65d21e11dce7f550defe1fd6d158389
+SHA512 (AdaCore-cvc5-98b5fb70e8a94fd258bfc959c4a6fd0cc3537564.tar.gz) =
fe344218d2e4063bfc59a6abf94455de1e34527722086ba3fdd351a9c1179907e6c9b7d0743d1811bf0c9bd847b83f6025d04ac7f3fcb1fcfa62e3b6308792cd
+Size (AdaCore-cvc5-98b5fb70e8a94fd258bfc959c4a6fd0cc3537564.tar.gz) = 8898627 bytes
+BLAKE2s (AdaCore-why3-52b6a590ba9bfc64aa0d22b41715358f26124a1f.tar.gz) = 0c99837c17d11261f4a0d649b203cbca2f2450a6f794c212fb680d2a63d104c9
+SHA512 (AdaCore-why3-52b6a590ba9bfc64aa0d22b41715358f26124a1f.tar.gz) =
6f700514f63fef8c8a4684400d9a7353bdd55b816ef5b4f34d4f7163e87282d8b71cec36b7a4e60acc8b4db1eec6b9e33267e1fa50d4a176576728082a0c1e03
+Size (AdaCore-why3-52b6a590ba9bfc64aa0d22b41715358f26124a1f.tar.gz) = 7196387 bytes
+BLAKE2s (AdaCore-z3-7e79f0deb7c9d43f7637113be5b99391f14fcc2e.tar.gz) = 91b6519eca90397b0246e03e2f3b9dbf19f42a110d60c70b36b7efeb8ad94b8a
+SHA512 (AdaCore-z3-7e79f0deb7c9d43f7637113be5b99391f14fcc2e.tar.gz) = 0289f45b63cb1fedcae374b2b35ca308488e628c3516ee8c129bd6b43ebd6141aa7c5bae52b3d63c4db7068326c3566eed76acb059e4efb1f1dc694fc8647ced
+Size (AdaCore-z3-7e79f0deb7c9d43f7637113be5b99391f14fcc2e.tar.gz) = 5237981 bytes
+BLAKE2s (gcc-13.3.0.tar.xz) = d204b8987b4780b569f28226cbfff34ae27124e529857c36ff90d5d40ef0b511
+SHA512 (gcc-13.3.0.tar.xz) = ed5f2f4c6ed2c796fcf2c93707159e9dbd3ddb1ba063d549804dd68cdabbb6d550985ae1c8465ae9a336cfe29274a6eb0f42e21924360574ebd8e5d5c7c9a801
+Size (gcc-13.3.0.tar.xz) = 87909952 bytes
+BLAKE2s (spark2014-12db22e854defa9d1c993ef904af1e72330a68ca.tar.gz) = 32b2081dfd7bbb4442bc791848cc4900a8cb9214e69fce6b55ef3724b2c9b145
+SHA512 (spark2014-12db22e854defa9d1c993ef904af1e72330a68ca.tar.gz) = 17644c49e642b2e79cfe481414d12df5b27bad003cdabbb0c9e88f5eb1f8b705b159791612a2d5f720e67017f0867ffaa5cfa0bc5fae8188442cd15fb456890b
+Size (spark2014-12db22e854defa9d1c993ef904af1e72330a68ca.tar.gz) = 11924977 bytes
+SHA1 (patch-Makefile) = e27afdf221bd7d527ba2e2d1046d67690319481c
+SHA1 (patch-gnatprove.gpr) = 7ee0cb8d24c8b063431d5ecd8a4e1291a48c5980
+SHA1 (patch-spark2014vsn.ads) = ab6a841bf7398c2f3b8df312463cbbcc59a02808
+SHA1 (patch-src_common_platform.ads) = a81254a67a3a847e1d1de35b310d1b8d9a442c69
+SHA1 (patch-src_common_semaphores__c.c) = 70f91a26919bca7772c35cbf211b38ab5c4cadd3
+SHA1 (patch-src_common_x86__64-netbsd_platform.adb) = eda3cf7f68c989280f9e684e9a5d9188ef41e690
+SHA1 (patch-src_gnatprove_spark__report.adb) = ef2941bb82881ab1f718dfec72764871c672f965
+SHA1 (patch-why3_Makefile.in) = 5d8385d634f1d4385109ec11ce5c239df85b2f51
Index: pkgsrc/lang/spark2014-13/patches/patch-Makefile
diff -u /dev/null pkgsrc/lang/spark2014-13/patches/patch-Makefile:1.1
--- /dev/null Thu Jul 10 12:43:03 2025
+++ pkgsrc/lang/spark2014-13/patches/patch-Makefile Thu Jul 10 12:43:03 2025
@@ -0,0 +1,66 @@
+$NetBSD: patch-Makefile,v 1.1 2025/07/10 12:43:03 dkazankov Exp $
+
+Fix install directory, build type, version number and NetBSD sha256sum
+
+--- Makefile.orig 2023-01-05 11:22:11.000000000 +0200
++++ Makefile
+@@ -41,7 +41,9 @@
+ install-all why3 all setup all-nightly doc-nightly run-benchmark \
+ create-benchmark
+
+-INSTALLDIR=$(CURDIR)/install
++PREFIX=
++DESTDIR=
++INSTALLDIR=$(DESTDIR)$(PREFIX)
+ SHAREDIR=$(INSTALLDIR)/share
+ SIDDIR=$(SHAREDIR)/gnat2why-sids
+ INCLUDEDIR=$(INSTALLDIR)/include/spark
+@@ -55,9 +57,10 @@
+ DOC=ug lrm
+ # Control if gnatprove is built in production or debug mode
+ PROD=-XBuild=Production
++GPRARGS='$(PROD)'
+ CP=cp -pr
+ MV=mv -f
+-VERSION=0.0w
++VERSION='FSF 13.0'
+
+ # main target for developers
+ all: gnat2why gnatprove why3
+@@ -78,7 +81,7 @@
+ # install-all install of gnatprove and why3
+
+ setup:
+- cd why3 && ./configure --prefix=$(INSTALLDIR)/libexec/spark \
++ cd why3 && ./configure --prefix=$(PREFIX)/libexec/spark \
+ --enable-relocation --disable-js-of-ocaml \
+ --disable-hypothesis-selection --disable-re
+
+@@ -89,15 +92,16 @@
+ install-all:
+ $(MAKE) install
+ $(MAKE) -C why3 install_spark2014_dev
+- sha256sum install/libexec/spark/bin/gnatwhy3 | cut -d' ' -f1 > install/libexec/spark/bin/gnatwhy3.hash
++ sha256 -n $(INSTALLDIR)/libexec/spark/bin/gnatwhy3 | cut -d' ' -f1 > $(INSTALLDIR)/libexec/spark/bin/gnatwhy3.hash
+ # Create the fake prover scripts to help extract benchmarks.
+- $(CP) benchmark_script/fake_* install/libexec/spark/bin
++ $(CP) benchmark_script/fake_* $(INSTALLDIR)/libexec/spark/bin
+
+ install:
+ mkdir -p $(INSTALLDIR)/bin $(CONFIGDIR) $(THEORIESDIR) \
+ $(RUNTIMESDIR) $(INCLUDEDIR) $(LIBDIR)
+ @echo "Generate default target.atp in $(INSTALLDIR)/bin:"
+ gcc -c -gnats spark2014vsn.ads -gnatet=$(INSTALLDIR)/bin/target.atp
++ $(CP) install/bin/* $(INSTALLDIR)/bin
+ $(CP) share/spark/help.txt $(GNATPROVEDIR)
+ $(CP) share/spark/config/* $(CONFIGDIR)
+ $(CP) share/spark/theories/*why $(THEORIESDIR)
+@@ -131,7 +135,7 @@
+ # This script should be run *ONLY* in developer build not in prod
+ # (gnat2why-nightly)
+ python3 scripts/why3keywords.py why3/src/core/keywords.ml src/why/why-keywords.adb
+- $(MAKE) -C gnat2why
++ $(MAKE) -C gnat2why AUTOMATED=1 GPRARGS=$(GPRARGS)
+ # (The timestamp of) src/why/xgen/gnat_ast.ml is updated every time `make` is called in
+ # `gnat2why`, causing a recompilation of why3 every time because Why3's makefile is
+ # based on timestamps not file content. So we check if anything changed before copying.
Index: pkgsrc/lang/spark2014-13/patches/patch-gnatprove.gpr
diff -u /dev/null pkgsrc/lang/spark2014-13/patches/patch-gnatprove.gpr:1.1
--- /dev/null Thu Jul 10 12:43:03 2025
+++ pkgsrc/lang/spark2014-13/patches/patch-gnatprove.gpr Thu Jul 10 12:43:03 2025
@@ -0,0 +1,17 @@
+$NetBSD: patch-gnatprove.gpr,v 1.1 2025/07/10 12:43:03 dkazankov Exp $
+
+Add libpthread link on NetBSD
+
+--- gnatprove.gpr.orig 2023-01-05 11:22:11.000000000 +0200
++++ gnatprove.gpr
+@@ -61,6 +61,10 @@
+ case Target is
+ when "x86-linux" | "x86_64-linux" =>
+ for Default_Switches ("Ada") use ("-pthread");
++ when "x86_64-netbsd" =>
++ for Default_Switches ("Ada") use ("-lpthread");
++ for Default_Switches ("C") use ("-lpthread");
++ for Linker_Options use ("-lpthread");
+ when others =>
+ null;
+ end case;
Index: pkgsrc/lang/spark2014-13/patches/patch-spark2014vsn.ads
diff -u /dev/null pkgsrc/lang/spark2014-13/patches/patch-spark2014vsn.ads:1.1
--- /dev/null Thu Jul 10 12:43:03 2025
+++ pkgsrc/lang/spark2014-13/patches/patch-spark2014vsn.ads Thu Jul 10 12:43:03 2025
@@ -0,0 +1,15 @@
+$NetBSD: patch-spark2014vsn.ads,v 1.1 2025/07/10 12:43:03 dkazankov Exp $
+
+Fix version number
+
+--- spark2014vsn.ads.orig 2023-01-05 11:22:11.000000000 +0200
++++ spark2014vsn.ads
+@@ -22,7 +22,7 @@
+
+ package SPARK2014VSN is
+
+- SPARK2014_Static_Version_String : constant String := "0.0w";
++ SPARK2014_Static_Version_String : constant String := "FSF 13.0";
+ -- Static string identifying this version, that can be used as an argument
+ -- to e.g. pragma Ident.
+ --
Index: pkgsrc/lang/spark2014-13/patches/patch-src_common_platform.ads
diff -u /dev/null pkgsrc/lang/spark2014-13/patches/patch-src_common_platform.ads:1.1
--- /dev/null Thu Jul 10 12:43:03 2025
+++ pkgsrc/lang/spark2014-13/patches/patch-src_common_platform.ads Thu Jul 10 12:43:03 2025
@@ -0,0 +1,15 @@
+$NetBSD: patch-src_common_platform.ads,v 1.1 2025/07/10 12:43:03 dkazankov Exp $
+
+Add NetBSD support
+
+--- src/common/platform.ads.orig 2023-01-05 11:22:11.000000000 +0200
++++ src/common/platform.ads
+@@ -30,7 +30,7 @@
+
+ type Host_Operating_System_Flavor is
+ (X86_Windows, X86_64_Windows, X86_Linux, X86_64_Linux, X86_64_Darwin,
+- X86_64_FreeBSD, CodePeer_OS, AArch64_Darwin);
++ X86_64_FreeBSD, CodePeer_OS, AArch64_Darwin, X86_64_NetBSD);
+
+ function Get_OS_Flavor return Host_Operating_System_Flavor;
+
Index: pkgsrc/lang/spark2014-13/patches/patch-src_common_semaphores__c.c
diff -u /dev/null pkgsrc/lang/spark2014-13/patches/patch-src_common_semaphores__c.c:1.1
--- /dev/null Thu Jul 10 12:43:03 2025
+++ pkgsrc/lang/spark2014-13/patches/patch-src_common_semaphores__c.c Thu Jul 10 12:43:03 2025
@@ -0,0 +1,73 @@
+$NetBSD: patch-src_common_semaphores__c.c,v 1.1 2025/07/10 12:43:03 dkazankov Exp $
+
+Fix runtime error caused semaphore names on NetBSD
+
+--- src/common/semaphores_c.c.orig 2023-01-05 11:22:11.000000000 +0200
++++ src/common/semaphores_c.c
+@@ -30,8 +30,33 @@
+ #include <stdio.h>
+ #include <stdlib.h>
+
++#if defined (__NetBSD__)
++char* __netbsd_sem_name(const char *name) {
++ size_t len = strlen (name);
++ char *sem_name = calloc (len+2, sizeof(char));
++ if (sem_name == NULL) {
++ return (char *) name;
++ }
++ char *p = sem_name;
++ if (len > 0 && name[0] != '/') {
++ sem_name[0] = '/';
++ p++;
++ }
++ strcpy (p, name);
++ return sem_name;
++}
++#endif
++
+ sem_t* create_semaphore (const char *name, unsigned int init) {
++#if defined (__NetBSD__)
++ char *sem_name = __netbsd_sem_name (name);
++ sem_t* r = sem_open (sem_name, O_CREAT | O_EXCL, 0600, init);
++ if (sem_name != name) {
++ free (sem_name);
++ }
++#else
+ sem_t* r = sem_open (name, O_CREAT | O_EXCL, 0600, init);
++#endif
+ if (r == SEM_FAILED) {
+ perror("failed to create semaphore");
+ exit(1);
+@@ -40,7 +65,15 @@
+ }
+
+ sem_t* open_semaphore (const char *name) {
++#if defined (__NetBSD__)
++ char *sem_name = __netbsd_sem_name (name);
++ sem_t* r = sem_open (sem_name, 0);
++ if (sem_name != name) {
++ free (sem_name);
++ }
++#else
+ sem_t* r = sem_open (name, 0);
++#endif
+ if (r == SEM_FAILED) {
+ perror("failed to open semaphore");
+ exit(1);
+@@ -70,7 +103,16 @@
+ }
+
+ void delete_semaphore (const char *name) {
++#if defined (__NetBSD__)
++ char *sem_name = __netbsd_sem_name (name);
++ int r = sem_unlink (sem_name);
++ if (sem_name != name) {
++ free (sem_name);
++ }
++ if (r == -1) {
++#else
+ if (sem_unlink(name) == -1) {
++#endif
+ // ignore errors of deleting on purpose
+ }
+ }
Index: pkgsrc/lang/spark2014-13/patches/patch-src_common_x86__64-netbsd_platform.adb
diff -u /dev/null pkgsrc/lang/spark2014-13/patches/patch-src_common_x86__64-netbsd_platform.adb:1.1
--- /dev/null Thu Jul 10 12:43:03 2025
+++ pkgsrc/lang/spark2014-13/patches/patch-src_common_x86__64-netbsd_platform.adb Thu Jul 10 12:43:03 2025
@@ -0,0 +1,44 @@
+$NetBSD: patch-src_common_x86__64-netbsd_platform.adb,v 1.1 2025/07/10 12:43:03 dkazankov Exp $
+
+Add NetBSD support
+
+--- /dev/null
++++ src/common/x86_64-netbsd/platform.adb
+@@ -0,0 +1,37 @@
++------------------------------------------------------------------------------
++-- --
++-- GNATPROVE COMPONENTS --
++-- --
++-- P L A T F O R M --
++-- --
++-- B o d y --
++-- --
++-- Copyright (C) 2010-2023, AdaCore --
++-- --
++-- gnatprove is free software; you can redistribute it and/or modify it --
++-- under terms of the GNU General Public License as published by the Free --
++-- Software Foundation; either version 3, or (at your option) any later --
++-- version. gnatprove is distributed in the hope that it will be useful, --
++-- but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHAN- --
++-- TABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public --
++-- License for more details. You should have received a copy of the GNU --
++-- General Public License distributed with gnatprove; see file COPYING3. --
++-- If not, go to http://www.gnu.org/licenses for a complete copy of the --
++-- license. --
++-- --
++-- gnatprove is maintained by AdaCore (http://www.adacore.com) --
++-- --
++------------------------------------------------------------------------------
++
++package body Platform is
++
++ -------------------
++ -- Get_OS_Flavor --
++ -------------------
++
++ function Get_OS_Flavor return Host_Operating_System_Flavor is
++ begin
++ return X86_64_NetBSD;
++ end Get_OS_Flavor;
++
++end Platform;
Index: pkgsrc/lang/spark2014-13/patches/patch-src_gnatprove_spark__report.adb
diff -u /dev/null pkgsrc/lang/spark2014-13/patches/patch-src_gnatprove_spark__report.adb:1.1
--- /dev/null Thu Jul 10 12:43:03 2025
+++ pkgsrc/lang/spark2014-13/patches/patch-src_gnatprove_spark__report.adb Thu Jul 10 12:43:03 2025
@@ -0,0 +1,14 @@
+$NetBSD: patch-src_gnatprove_spark__report.adb,v 1.1 2025/07/10 12:43:03 dkazankov Exp $
+
+Add NetBSD support
+
+--- src/gnatprove/spark_report.adb.orig 2023-01-05 11:22:11.000000000 +0200
++++ src/gnatprove/spark_report.adb
+@@ -1086,6 +1086,7 @@
+ when X86_Linux | X86_64_Linux => "Linux",
+ when X86_64_Darwin => "Darwin",
+ when X86_64_FreeBSD => "FreeBSD",
++ when X86_64_NetBSD => "NetBSD",
+ when CodePeer_OS => "CodePeer OS",
+ when AArch64_Darwin => "Darwin");
+
Index: pkgsrc/lang/spark2014-13/patches/patch-why3_Makefile.in
diff -u /dev/null pkgsrc/lang/spark2014-13/patches/patch-why3_Makefile.in:1.1
--- /dev/null Thu Jul 10 12:43:03 2025
+++ pkgsrc/lang/spark2014-13/patches/patch-why3_Makefile.in Thu Jul 10 12:43:03 2025
@@ -0,0 +1,15 @@
+$NetBSD: patch-why3_Makefile.in,v 1.1 2025/07/10 12:43:03 dkazankov Exp $
+
+NetBSD doesn't have -C option
+
+--- why3/Makefile.in.orig 2022-12-21 10:10:00.000000000 +0200
++++ why3/Makefile.in
+@@ -844,7 +844,7 @@
+ $(INSTALL_DATA) share/images/*.png $(DATADIR)/why3/images
+ $(MKDIR_P) $(DATADIR)/why3/lang
+ # Install all Why3 tools
+- for f in bin/why3*.@OCAMLBEST@; do install -C "$$f" $(BINDIR)/"$$(basename "$$f" .@OCAMLBEST@)$(EXE)"; done
++ for f in bin/why3*.@OCAMLBEST@; do install "$$f" $(BINDIR)/"$$(basename "$$f" .@OCAMLBEST@)$(EXE)"; done
+ # Install lang files for Why3 IDE
+ for f in share/lang/*.lang; do $(INSTALL_DATA) "$$f" "$(DATADIR)/why3/lang/$$(basename $$f)"; done
+
Home |
Main Index |
Thread Index |
Old Index