pkgsrc-WIP-changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
lang/spark2014: Add 13.0.0
Module Name: pkgsrc-wip
Committed By: Dmytro Kazankov <dmytro.kazankov%gmail.com@localhost>
Pushed By: dkazankov
Date: Tue May 21 12:32:21 2024 +0300
Changeset: 780d088fe590becf9ac88b8452f74d325a637d46
Added Files:
spark2014/DESCR
spark2014/Makefile
spark2014/PLIST
spark2014/buildlink3.mk
spark2014/distinfo
spark2014/patches/patch-Makefile
spark2014/patches/patch-gnatprove.gpr
spark2014/patches/patch-spark2014vsn.ads
spark2014/patches/patch-src_common_platform.ads
spark2014/patches/patch-src_common_x86__64-netbsd_platform.adb
spark2014/patches/patch-src_gnatprove_spark__report.adb
spark2014/patches/patch-why3_Makefile.in
spark2014/version.mk
Log Message:
lang/spark2014: Add 13.0.0
* gnatprove tool - it is mostly a subset of the Ada language that is used
to prove the correctness of programs.
* The package major version matches corresponding GCC version and is
the latest (more precisely the only) fsf-13 branch version.
To see a diff of this commit:
https://wip.pkgsrc.org/cgi-bin/gitweb.cgi?p=pkgsrc-wip.git;a=commitdiff;h=780d088fe590becf9ac88b8452f74d325a637d46
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
diffstat:
spark2014/DESCR | 8 +
spark2014/Makefile | 95 ++++
spark2014/PLIST | 610 +++++++++++++++++++++
spark2014/buildlink3.mk | 17 +
spark2014/distinfo | 27 +
spark2014/patches/patch-Makefile | 66 +++
spark2014/patches/patch-gnatprove.gpr | 27 +
spark2014/patches/patch-spark2014vsn.ads | 15 +
spark2014/patches/patch-src_common_platform.ads | 15 +
.../patch-src_common_x86__64-netbsd_platform.adb | 44 ++
.../patches/patch-src_gnatprove_spark__report.adb | 14 +
spark2014/patches/patch-why3_Makefile.in | 15 +
spark2014/version.mk | 3 +
13 files changed, 956 insertions(+)
diffs:
diff --git a/spark2014/DESCR b/spark2014/DESCR
new file mode 100644
index 0000000000..81e09a4aba
--- /dev/null
+++ b/spark2014/DESCR
@@ -0,0 +1,8 @@
+SPARK 2014 toolset
+
+SPARK is a software development technology specifically designed for
+engineering high-reliability applications.
+It consists of a programming language, a verification toolset and a design
+method which, taken together, ensure that ultra-low defect software can be
+deployed in application domains where high-reliability must be assured
+and where safety and security are key requirements.
diff --git a/spark2014/Makefile b/spark2014/Makefile
new file mode 100644
index 0000000000..19915ce02d
--- /dev/null
+++ b/spark2014/Makefile
@@ -0,0 +1,95 @@
+# $NetBSD: Makefile,v 1.3 2024/05/02 14:00:00 dkazankov Exp $
+
+.include "version.mk"
+PKGNAME= spark2014-${SPARK2014_VERSION}
+CATEGORIES= lang devel
+MAINTAINER= pkgsrc-users%NetBSD.org@localhost
+HOMEPAGE= https://github.com/AdaCore/spark2014
+COMMENT= SPARK 2014 toolset
+LICENSE= gnu-gpl-v3
+
+USE_LANGUAGES= c ada
+USE_TOOLS+= gmake
+HAS_CONFIGURE= yes
+
+MKPIE_SUPPORTED= no
+RELRO_SUPPORTED= no
+
+.include "../../mk/bsd.prefs.mk"
+
+DISTNAME= spark2014-${PKGVERSION_NOREV}
+GITHUB_PROJECT= spark2014
+MASTER_SITES= ${MASTER_SITE_GITHUB:=AdaCore/}
+DISTFILES= ${DEFAULT_DISTFILES}
+
+# latest fsf-13 branch commit
+GITHUB_TAG= 12db22e854defa9d1c993ef904af1e72330a68ca
+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
+
+GCC_DIST_VERSION= 13.2.0
+GCC_DISTNAME= gcc-${GCC_DIST_VERSION}
+GCC_EXTRACT_SUFFIX= .tar.xz
+GCC_DISTFILE= ${GCC_DISTNAME}${GCC_EXTRACT_SUFFIX}
+
+DISTFILES+= ${GCC_DISTFILE}
+SITES.${GCC_DISTFILE}= ${MASTER_SITE_GNU:=gcc/${GCC_DISTNAME}/}
+
+GCC_REQD+= 13
+
+.include "../../wip/gprbuild/buildlink3.mk"
+.include "../../wip/xmlada/buildlink3.mk"
+.include "../../wip/gprlib/buildlink3.mk"
+.include "../../wip/gnatcoll-core/buildlink3.mk"
+
+PYTHON_VERSIONS_ACCEPTED= 312 311 310 39 38
+.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 "../../wip/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"
+
+CONFIG_SHELL= ${MAKE_PROGRAM}
+CONFIGURE_ARGS+= DESTDIR=${DESTDIR} PREFIX=${PREFIX}
+CONFIGURE_SCRIPT= setup
+
+MAKE_FLAGS+= DESTDIR=${DESTDIR} PREFIX=${PREFIX}
+
+INSTALL_TARGET= install-all
+
+SUBST_CLASSES+= interpreter
+SUBST_STAGE.interpreter= pre-configure
+SUBST_FILES.interpreter= benchmark_script/*
+SUBST_MESSAGE.interpreter= Fix interpreter
+SUBST_SED.interpreter= -e 's,/bin/bash,/bin/sh,g'
+
+GENERATE_PLIST+= \
+ cd ${DESTDIR}${PREFIX} && \
+ ${FIND} bin \( -type f -or -type l \) -print | ${SORT};
+
+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 ./*
+
+.include "../../mk/bsd.pkg.mk"
diff --git a/spark2014/PLIST b/spark2014/PLIST
new file mode 100644
index 0000000000..8cf0e33229
--- /dev/null
+++ b/spark2014/PLIST
@@ -0,0 +1,610 @@
+@comment $NetBSD: PLIST,v 1.0 2024/05/06 11:00:00 dkazankov Exp $
+bin/gnat2why
+bin/gnatprove
+bin/spark_memcached_wrapper
+bin/spark_report
+bin/spark_semaphore_wrapper
+bin/target.atp
+include/spark/spark-big_integers.ads
+include/spark/spark-big_integers__light.adb
+include/spark/spark-big_integers__light.ads
+include/spark/spark-big_intervals.ads
+include/spark/spark-big_intervals__light.ads
+include/spark/spark-big_reals.ads
+include/spark/spark-big_reals__light.adb
+include/spark/spark-big_reals__light.ads
+include/spark/spark-containers-formal-doubly_linked_lists.adb
+include/spark/spark-containers-formal-doubly_linked_lists.ads
+include/spark/spark-containers-formal-hashed_maps.adb
+include/spark/spark-containers-formal-hashed_maps.ads
+include/spark/spark-containers-formal-hashed_sets.adb
+include/spark/spark-containers-formal-hashed_sets.ads
+include/spark/spark-containers-formal-holders.adb
+include/spark/spark-containers-formal-holders.ads
+include/spark/spark-containers-formal-ordered_maps.adb
+include/spark/spark-containers-formal-ordered_maps.ads
+include/spark/spark-containers-formal-ordered_sets.adb
+include/spark/spark-containers-formal-ordered_sets.ads
+include/spark/spark-containers-formal-unbounded_doubly_linked_lists.adb
+include/spark/spark-containers-formal-unbounded_doubly_linked_lists.ads
+include/spark/spark-containers-formal-unbounded_hashed_maps.adb
+include/spark/spark-containers-formal-unbounded_hashed_maps.ads
+include/spark/spark-containers-formal-unbounded_hashed_sets.adb
+include/spark/spark-containers-formal-unbounded_hashed_sets.ads
+include/spark/spark-containers-formal-unbounded_ordered_maps.adb
+include/spark/spark-containers-formal-unbounded_ordered_maps.ads
+include/spark/spark-containers-formal-unbounded_ordered_sets.adb
+include/spark/spark-containers-formal-unbounded_ordered_sets.ads
+include/spark/spark-containers-formal-unbounded_vectors.adb
+include/spark/spark-containers-formal-unbounded_vectors.ads
+include/spark/spark-containers-formal-vectors.adb
+include/spark/spark-containers-formal-vectors.ads
+include/spark/spark-containers-formal.ads
+include/spark/spark-containers-functional-base.adb
+include/spark/spark-containers-functional-base.ads
+include/spark/spark-containers-functional-infinite_sequences.adb
+include/spark/spark-containers-functional-infinite_sequences.ads
+include/spark/spark-containers-functional-infinite_sequences__light.adb
+include/spark/spark-containers-functional-infinite_sequences__light.ads
+include/spark/spark-containers-functional-maps.adb
+include/spark/spark-containers-functional-maps.ads
+include/spark/spark-containers-functional-maps__light.adb
+include/spark/spark-containers-functional-maps__light.ads
+include/spark/spark-containers-functional-multisets.adb
+include/spark/spark-containers-functional-multisets.ads
+include/spark/spark-containers-functional-multisets__light.adb
+include/spark/spark-containers-functional-multisets__light.ads
+include/spark/spark-containers-functional-sets.adb
+include/spark/spark-containers-functional-sets.ads
+include/spark/spark-containers-functional-sets__light.adb
+include/spark/spark-containers-functional-sets__light.ads
+include/spark/spark-containers-functional-vectors.adb
+include/spark/spark-containers-functional-vectors.ads
+include/spark/spark-containers-functional-vectors__light.adb
+include/spark/spark-containers-functional-vectors__light.ads
+include/spark/spark-containers-functional.ads
+include/spark/spark-containers-parameter_checks.adb
+include/spark/spark-containers-parameter_checks.ads
+include/spark/spark-containers-stable_sorting.adb
+include/spark/spark-containers-stable_sorting.ads
+include/spark/spark-containers-types.ads
+include/spark/spark-containers-types__light.ads
+include/spark/spark-containers.ads
+include/spark/spark-containers__exec.ads
+include/spark/spark-conversions-float_conversions.ads
+include/spark/spark-conversions-long_float_conversions.ads
+include/spark/spark-conversions-long_integer_conversions.ads
+include/spark/spark-conversions.ads
+include/spark/spark-cut_operations.adb
+include/spark/spark-cut_operations.ads
+include/spark/spark-higher_order-fold.adb
+include/spark/spark-higher_order-fold.ads
+include/spark/spark-higher_order.adb
+include/spark/spark-higher_order.ads
+include/spark/spark-lemmas-arithmetic.adb
+include/spark/spark-lemmas-arithmetic.ads
+include/spark/spark-lemmas-constrained_array.adb
+include/spark/spark-lemmas-constrained_array.ads
+include/spark/spark-lemmas-fixed_point_arithmetic.adb
+include/spark/spark-lemmas-fixed_point_arithmetic.ads
+include/spark/spark-lemmas-float_arithmetic.ads
+include/spark/spark-lemmas-float_base.ads
+include/spark/spark-lemmas-floating_point_arithmetic.adb
+include/spark/spark-lemmas-floating_point_arithmetic.ads
+include/spark/spark-lemmas-integer_arithmetic.ads
+include/spark/spark-lemmas-long_float_arithmetic.ads
+include/spark/spark-lemmas-long_integer_arithmetic.ads
+include/spark/spark-lemmas-mod32_arithmetic.ads
+include/spark/spark-lemmas-mod64_arithmetic.ads
+include/spark/spark-lemmas-mod_arithmetic.adb
+include/spark/spark-lemmas-mod_arithmetic.ads
+include/spark/spark-lemmas-unconstrained_array.adb
+include/spark/spark-lemmas-unconstrained_array.ads
+include/spark/spark-lemmas.ads
+include/spark/spark-pointers-abstract_maps.ads
+include/spark/spark-pointers-pointers_with_aliasing.adb
+include/spark/spark-pointers-pointers_with_aliasing.ads
+include/spark/spark-pointers-pointers_with_aliasing_separate_memory.adb
+include/spark/spark-pointers-pointers_with_aliasing_separate_memory.ads
+include/spark/spark-pointers.ads
+include/spark/spark-tests-array_lemmas.adb
+include/spark/spark-tests-array_lemmas.ads
+include/spark/spark-tests.ads
+include/spark/spark.ads
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_is_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_protect__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_protect__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_scale__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_scale__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_is_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_protect__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_protect__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_scale__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_scale__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.v
+lib/gnat/proof/Coq/Ada___ada___spark__tests__array_lemmas__test_ufloat__lemma_transitive_order__pragargs__forall.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__tests__array_lemmas__test_ufloat__lemma_transitive_order__pragargs__forall.v
+lib/gnat/proof/Coq/Ada___ada___spark__tests__array_lemmas__test_uint__lemma_transitive_order__pragargs__forall.ctx
+lib/gnat/proof/Coq/Ada___ada___spark__tests__array_lemmas__test_uint__lemma_transitive_order__pragargs__forall.v
+lib/gnat/proof/Coq/common/float32_div_common.prf
+lib/gnat/proof/Coq/common/float32_mul_common.prf
+lib/gnat/proof/Coq/common/float64_div_common.prf
+lib/gnat/proof/Coq/common/float64_mul_common.prf
+lib/gnat/proof/Coq/common/float_div_is_monotonic.prf
+lib/gnat/proof/Coq/common/float_div_right_negative_is_monotonic.prf
+lib/gnat/proof/Coq/common/float_mult_by_less_than_one.prf
+lib/gnat/proof/Coq/common/float_mult_is_monotonic.prf
+lib/gnat/proof/Coq/common/float_mult_right_negative_is_monotonic.prf
+lib/gnat/proof/Coq/common/lemma_exp_monotonic.prf
+lib/gnat/proof/Coq/common/lemma_mod_symmetry.prf
+lib/gnat/proof/Coq/common/lemma_modular_div_is_monotonic.prf
+lib/gnat/proof/Coq/common/lemma_modular_div_then_mult_bounds_part1.prf
+lib/gnat/proof/Coq/common/lemma_modular_div_then_mult_bounds_part2.prf
+lib/gnat/proof/Coq/common/lemma_modular_mult_is_monotonic.prf
+lib/gnat/proof/Coq/common/lemma_modular_mult_is_strictly_monotonic.prf
+lib/gnat/proof/Coq/common/lemma_modular_mult_protect.prf
+lib/gnat/proof/Coq/common/lemma_modular_mult_scale.prf
+lib/gnat/proof/Coq/common/lemma_modular_mult_then_div_is_ident.prf
+lib/gnat/proof/Coq/common/lemma_modular_mult_then_mod_is_zero.prf
+lib/gnat/proof/Coq/common/lemma_mult_protect.prf
+lib/gnat/proof/Coq/common/lemma_raising_order_float.prf
+lib/gnat/proof/Coq/common/lemma_raising_order_int.prf
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__is_float/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__is_float__2/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__is_integer/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__is_integer_32/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__is_integer_64/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_add_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_div_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_div_left_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_div_right_negative_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_integer_add_exact/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_integer_mul_exact/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_integer_sub_exact/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_mult_by_less_than_one/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_mult_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_mult_right_negative_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_rounding_error_add/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_rounding_error_div/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_rounding_error_mul/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_rounding_error_sub/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__lemma_sub_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_div_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_div_right_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_exp_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_exp_is_monotonic_2/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mod_range/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mod_symmetry/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mult_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mult_is_strictly_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mult_protect/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mult_scale/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mult_then_div_is_ident/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__integer_arithmetic__lemma_mult_then_mod_is_zero/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__is_float/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__is_float__2/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__is_integer/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__is_integer_32/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__is_integer_64/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_add_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_left_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_right_negative_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_integer_add_exact/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_integer_mul_exact/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_integer_sub_exact/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_by_less_than_one/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_right_negative_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_rounding_error_add/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_rounding_error_div/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_rounding_error_mul/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_rounding_error_sub/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic__lemma_sub_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_div_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_div_right_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_exp_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_exp_is_monotonic_2/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mod_range/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mod_symmetry/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mult_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mult_is_strictly_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mult_protect/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mult_scale/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mult_then_div_is_ident/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mult_then_mod_is_zero/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_strictly_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_protect/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_scale/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_div_is_ident/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_mod_is_zero/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_strictly_monotonic/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_protect/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_scale/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_div_is_ident/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_mod_is_zero/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__tests__array_lemmas__test_transitive_order_float/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__tests__array_lemmas__test_transitive_order_float__2/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__tests__array_lemmas__test_transitive_order_int/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__tests__array_lemmas__test_transitive_order_int__2/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__tests__array_lemmas__test_ufloat__lemma_transitive_order/why3session.xml
+lib/gnat/proof/sessions/ada___ada___spark__tests__array_lemmas__test_uint__lemma_transitive_order/why3session.xml
+lib/gnat/proof/sessions/ada___spark__big_intervals__in_range/why3session.xml
+lib/gnat/proof/sessions/ada___spark__big_intervals__next/why3session.xml
+lib/gnat/sparklib.gpr
+lib/gnat/sparklib_common.gpr
+lib/gnat/sparklib_internal.gpr
+lib/gnat/sparklib_light.gpr
+libexec/spark/bin/fake_alt-ergo
+libexec/spark/bin/fake_cvc4
+libexec/spark/bin/fake_cvc5
+libexec/spark/bin/fake_z3
+libexec/spark/bin/gnat_server
+libexec/spark/bin/gnatwhy3
+libexec/spark/bin/gnatwhy3.hash
+libexec/spark/bin/why3
+${PLIST.ocaml-opt}libexec/spark/bin/why3config.cmxs
+libexec/spark/bin/why3cpulimit
+${PLIST.ocaml-opt}libexec/spark/bin/why3realize.cmxs
+libexec/spark/bin/why3server
+${PLIST.ocaml-opt}libexec/spark/bin/why3session.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/commands/why3config.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/commands/why3doc.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/commands/why3execute.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/commands/why3extract.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/commands/why3pp.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/commands/why3prove.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/commands/why3realize.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/commands/why3replay.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/commands/why3session.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/commands/why3shell.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/commands/why3show.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/commands/why3wc.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/commands/why3webserver.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/plugins/ada_terms.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/plugins/cfg.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/plugins/dimacs.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/plugins/genequlin.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/plugins/gnat_json.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/plugins/microc.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/plugins/python.cmxs
+${PLIST.ocaml-opt}libexec/spark/lib/why3/plugins/tptp.cmxs
+libexec/spark/lib/why3/why3-call-pvs
+libexec/spark/lib/why3/why3cpulimit
+libexec/spark/lib/why3/why3server
+libexec/spark/share/why3/drivers/alt-ergo_gnatprove.drv
+libexec/spark/share/why3/drivers/alt_ergo.drv
+libexec/spark/share/why3/drivers/alt_ergo_2_2_0.drv
+libexec/spark/share/why3/drivers/alt_ergo_2_3.drv
+libexec/spark/share/why3/drivers/alt_ergo_common.drv
+libexec/spark/share/why3/drivers/alt_ergo_fp.drv
+libexec/spark/share/why3/drivers/alt_ergo_model.drv
+libexec/spark/share/why3/drivers/alt_ergo_smt2.drv
+libexec/spark/share/why3/drivers/beagle.drv
+libexec/spark/share/why3/drivers/colibri.drv
+libexec/spark/share/why3/drivers/colibri2.drv
+libexec/spark/share/why3/drivers/coq-common.gen
+libexec/spark/share/why3/drivers/coq-realizations.aux
+libexec/spark/share/why3/drivers/coq-realize.drv
+libexec/spark/share/why3/drivers/coq-ssreflect.drv
+libexec/spark/share/why3/drivers/coq.drv
+libexec/spark/share/why3/drivers/coq_gnatprove.drv
+libexec/spark/share/why3/drivers/cvc3.drv
+libexec/spark/share/why3/drivers/cvc4-realize.drv
+libexec/spark/share/why3/drivers/cvc4.drv
+libexec/spark/share/why3/drivers/cvc4_14.drv
+libexec/spark/share/why3/drivers/cvc4_15.drv
+libexec/spark/share/why3/drivers/cvc4_15_counterexample.drv
+libexec/spark/share/why3/drivers/cvc4_16.drv
+libexec/spark/share/why3/drivers/cvc4_16.gen
+libexec/spark/share/why3/drivers/cvc4_16_counterexample.drv
+libexec/spark/share/why3/drivers/cvc4_17.drv
+libexec/spark/share/why3/drivers/cvc4_17_counterexample.drv
+libexec/spark/share/why3/drivers/cvc4_18_strings.drv
+libexec/spark/share/why3/drivers/cvc4_18_strings_counterexample.drv
+libexec/spark/share/why3/drivers/cvc4_bv.gen
+libexec/spark/share/why3/drivers/cvc4_gnatprove.drv
+libexec/spark/share/why3/drivers/cvc4_gnatprove_ce.drv
+libexec/spark/share/why3/drivers/cvc4_gnatprove_extra_axioms.drv
+libexec/spark/share/why3/drivers/cvc4_gnatprove_oldfloat.drv
+libexec/spark/share/why3/drivers/cvc4_gnatprove_qf.drv
+libexec/spark/share/why3/drivers/cvc5.drv
+libexec/spark/share/why3/drivers/cvc5_counterexample.drv
+libexec/spark/share/why3/drivers/cvc5_gnatprove.drv
+libexec/spark/share/why3/drivers/cvc5_gnatprove_ce.drv
+libexec/spark/share/why3/drivers/discrimination.gen
+libexec/spark/share/why3/drivers/eprover.drv
+libexec/spark/share/why3/drivers/gappa.drv
+libexec/spark/share/why3/drivers/iprover.drv
+libexec/spark/share/why3/drivers/isabelle-common.gen
+libexec/spark/share/why3/drivers/isabelle-realizations.aux
+libexec/spark/share/why3/drivers/isabelle-realize.drv
+libexec/spark/share/why3/drivers/isabelle.drv
+libexec/spark/share/why3/drivers/mathematica.drv
+libexec/spark/share/why3/drivers/mathsat.drv
+libexec/spark/share/why3/drivers/metis.drv
+libexec/spark/share/why3/drivers/metitarski.drv
+libexec/spark/share/why3/drivers/no-bv.gen
+libexec/spark/share/why3/drivers/polypaver.drv
+libexec/spark/share/why3/drivers/princess.drv
+libexec/spark/share/why3/drivers/psyche.drv
+libexec/spark/share/why3/drivers/pvs-common.gen
+libexec/spark/share/why3/drivers/pvs-realizations.aux
+libexec/spark/share/why3/drivers/pvs-realize.drv
+libexec/spark/share/why3/drivers/pvs.drv
+libexec/spark/share/why3/drivers/safeprover.drv
+libexec/spark/share/why3/drivers/simplify.drv
+libexec/spark/share/why3/drivers/smt-libv2-bv-realization.gen
+libexec/spark/share/why3/drivers/smt-libv2-bv.gen
+libexec/spark/share/why3/drivers/smt-libv2-floats-gnatprove.gen
+libexec/spark/share/why3/drivers/smt-libv2-floats-int_via_bv.gen
+libexec/spark/share/why3/drivers/smt-libv2-floats-int_via_real.gen
+libexec/spark/share/why3/drivers/smt-libv2-floats.gen
+libexec/spark/share/why3/drivers/smt-libv2-gnatprove.gen
+libexec/spark/share/why3/drivers/smt-libv2.gen
+libexec/spark/share/why3/drivers/smtlib-strings.gen
+libexec/spark/share/why3/drivers/spass.drv
+libexec/spark/share/why3/drivers/spass_types.drv
+libexec/spark/share/why3/drivers/tptp-tff0.drv
+libexec/spark/share/why3/drivers/tptp-tff1.drv
+libexec/spark/share/why3/drivers/tptp.gen
+libexec/spark/share/why3/drivers/vampire-smt.drv
+libexec/spark/share/why3/drivers/vampire.drv
+libexec/spark/share/why3/drivers/verit.drv
+libexec/spark/share/why3/drivers/why3.drv
+libexec/spark/share/why3/drivers/why3_smt.drv
+libexec/spark/share/why3/drivers/why3_tptp.drv
+libexec/spark/share/why3/drivers/yices-smt2.drv
+libexec/spark/share/why3/drivers/yices.drv
+libexec/spark/share/why3/drivers/z3.drv
+libexec/spark/share/why3/drivers/z3_432.drv
+libexec/spark/share/why3/drivers/z3_440.drv
+libexec/spark/share/why3/drivers/z3_440_counterexample.drv
+libexec/spark/share/why3/drivers/z3_471.drv
+libexec/spark/share/why3/drivers/z3_471_counterexample.drv
+libexec/spark/share/why3/drivers/z3_471_nobv.drv
+libexec/spark/share/why3/drivers/z3_bv.gen
+libexec/spark/share/why3/drivers/z3_gnatprove.drv
+libexec/spark/share/why3/drivers/z3_gnatprove_ce.drv
+libexec/spark/share/why3/drivers/z3_no_quant.drv
+libexec/spark/share/why3/drivers/z3_smtv1.drv
+libexec/spark/share/why3/drivers/zenon.drv
+libexec/spark/share/why3/drivers/zenon_modulo.drv
+libexec/spark/share/why3/images/fatcow.rc
+libexec/spark/share/why3/images/fatcow/accept.png
+libexec/spark/share/why3/images/fatcow/bin.png
+libexec/spark/share/why3/images/fatcow/bomb.png
+libexec/spark/share/why3/images/fatcow/brick_delete.png
+libexec/spark/share/why3/images/fatcow/bullet_black.png
+libexec/spark/share/why3/images/fatcow/bullet_blue.png
+libexec/spark/share/why3/images/fatcow/bullet_green.png
+libexec/spark/share/why3/images/fatcow/bullet_red.png
+libexec/spark/share/why3/images/fatcow/bullet_white.png
+libexec/spark/share/why3/images/fatcow/cancel.png
+libexec/spark/share/why3/images/fatcow/control_pause_blue.png
+libexec/spark/share/why3/images/fatcow/control_play_blue.png
+libexec/spark/share/why3/images/fatcow/database_delete.png
+libexec/spark/share/why3/images/fatcow/ddr_memory.png
+libexec/spark/share/why3/images/fatcow/delete.png
+libexec/spark/share/why3/images/fatcow/exclamation.png
+libexec/spark/share/why3/images/fatcow/folder.png
+libexec/spark/share/why3/images/fatcow/help.png
+libexec/spark/share/why3/images/fatcow/magic_wand_2.png
+libexec/spark/share/why3/images/fatcow/multitool.png
+libexec/spark/share/why3/images/fatcow/package.png
+libexec/spark/share/why3/images/fatcow/pencil.png
+libexec/spark/share/why3/images/fatcow/readme-fatcow.txt
+libexec/spark/share/why3/images/fatcow/script.png
+libexec/spark/share/why3/images/fatcow/time_delete.png
+libexec/spark/share/why3/images/fatcow/timeline.png
+libexec/spark/share/why3/images/fatcow/update.png
+libexec/spark/share/why3/images/logo-why.png
+libexec/spark/share/why3/lang/why3.lang
+libexec/spark/share/why3/lang/why3c.lang
+libexec/spark/share/why3/lang/why3py.lang
+libexec/spark/share/why3/libs/coq/BuiltIn.v
+libexec/spark/share/why3/libs/coq/HighOrd.v
+libexec/spark/share/why3/libs/coq/SPARK.v
+libexec/spark/share/why3/libs/coq/_CoqProject
+libexec/spark/share/why3/libs/coq/bool/Bool.v
+libexec/spark/share/why3/libs/coq/bv/BV_Gen.v
+libexec/spark/share/why3/libs/coq/bv/Pow2int.v
+libexec/spark/share/why3/libs/coq/floating_point/Double.v
+libexec/spark/share/why3/libs/coq/floating_point/DoubleFormat.v
+libexec/spark/share/why3/libs/coq/floating_point/GenFloat.v
+libexec/spark/share/why3/libs/coq/floating_point/Rounding.v
+libexec/spark/share/why3/libs/coq/floating_point/Single.v
+libexec/spark/share/why3/libs/coq/floating_point/SingleFormat.v
+libexec/spark/share/why3/libs/coq/for_drivers/ComputerOfEuclideanDivision.v
+libexec/spark/share/why3/libs/coq/ieee_float/Float32.v
+libexec/spark/share/why3/libs/coq/ieee_float/Float64.v
+libexec/spark/share/why3/libs/coq/ieee_float/GenericFloat.v
+libexec/spark/share/why3/libs/coq/ieee_float/RoundingMode.v
+libexec/spark/share/why3/libs/coq/int/Abs.v
+libexec/spark/share/why3/libs/coq/int/ComputerDivision.v
+libexec/spark/share/why3/libs/coq/int/Div2.v
+libexec/spark/share/why3/libs/coq/int/EuclideanDivision.v
+libexec/spark/share/why3/libs/coq/int/Exponentiation.v
+libexec/spark/share/why3/libs/coq/int/Int.v
+libexec/spark/share/why3/libs/coq/int/MinMax.v
+libexec/spark/share/why3/libs/coq/int/NumOf.v
+libexec/spark/share/why3/libs/coq/int/Power.v
+libexec/spark/share/why3/libs/coq/list/Append.v
+libexec/spark/share/why3/libs/coq/list/Combine.v
+libexec/spark/share/why3/libs/coq/list/Distinct.v
+libexec/spark/share/why3/libs/coq/list/HdTl.v
+libexec/spark/share/why3/libs/coq/list/HdTlNoOpt.v
+libexec/spark/share/why3/libs/coq/list/Length.v
+libexec/spark/share/why3/libs/coq/list/List.v
+libexec/spark/share/why3/libs/coq/list/Mem.v
+libexec/spark/share/why3/libs/coq/list/Nth.v
+libexec/spark/share/why3/libs/coq/list/NthHdTl.v
+libexec/spark/share/why3/libs/coq/list/NthLength.v
+libexec/spark/share/why3/libs/coq/list/NthLengthAppend.v
+libexec/spark/share/why3/libs/coq/list/NthNoOpt.v
+libexec/spark/share/why3/libs/coq/list/NumOcc.v
+libexec/spark/share/why3/libs/coq/list/Permut.v
+libexec/spark/share/why3/libs/coq/list/RevAppend.v
+libexec/spark/share/why3/libs/coq/list/Reverse.v
+libexec/spark/share/why3/libs/coq/map/Const.v
+libexec/spark/share/why3/libs/coq/map/Map.v
+libexec/spark/share/why3/libs/coq/map/MapInjection.v
+libexec/spark/share/why3/libs/coq/map/MapPermut.v
+libexec/spark/share/why3/libs/coq/map/Occ.v
+libexec/spark/share/why3/libs/coq/number/Coprime.v
+libexec/spark/share/why3/libs/coq/number/Divisibility.v
+libexec/spark/share/why3/libs/coq/number/Gcd.v
+libexec/spark/share/why3/libs/coq/number/Parity.v
+libexec/spark/share/why3/libs/coq/number/Prime.v
+libexec/spark/share/why3/libs/coq/option/Option.v
+libexec/spark/share/why3/libs/coq/real/Abs.v
+libexec/spark/share/why3/libs/coq/real/ExpLog.v
+libexec/spark/share/why3/libs/coq/real/FromInt.v
+libexec/spark/share/why3/libs/coq/real/MinMax.v
+libexec/spark/share/why3/libs/coq/real/PowerInt.v
+libexec/spark/share/why3/libs/coq/real/PowerReal.v
+libexec/spark/share/why3/libs/coq/real/Real.v
+libexec/spark/share/why3/libs/coq/real/RealInfix.v
+libexec/spark/share/why3/libs/coq/real/Square.v
+libexec/spark/share/why3/libs/coq/real/Trigonometry.v
+libexec/spark/share/why3/libs/coq/real/Truncate.v
+libexec/spark/share/why3/libs/coq/set/Cardinal.v
+libexec/spark/share/why3/libs/coq/set/Fset.v
+libexec/spark/share/why3/libs/coq/set/FsetInduction.v
+libexec/spark/share/why3/libs/coq/set/FsetInt.v
+libexec/spark/share/why3/libs/coq/set/FsetSum.v
+libexec/spark/share/why3/libs/coq/set/Set.v
+libexec/spark/share/why3/libs/coq/set/SetApp.v
+libexec/spark/share/why3/libs/coq/set/SetAppInt.v
+libexec/spark/share/why3/libs/coq/set/SetImp.v
+libexec/spark/share/why3/libs/coq/set/SetImpInt.v
+libexec/spark/share/why3/libs/coq/spark/SPARK_Integer_Arithmetic.v
+libexec/spark/share/why3/libs/coq/spark/SPARK_Raising_Order.v
+libexec/spark/share/why3/libs/coq/version
+libexec/spark/share/why3/libs/coq/version.in
+libexec/spark/share/why3/provers-detection-data.conf
+libexec/spark/share/why3/theories/algebra.mlw
+libexec/spark/share/why3/theories/array.mlw
+libexec/spark/share/why3/theories/bag.mlw
+libexec/spark/share/why3/theories/bintree.mlw
+libexec/spark/share/why3/theories/bool.mlw
+libexec/spark/share/why3/theories/bv.mlw
+libexec/spark/share/why3/theories/byte_string.mlw
+libexec/spark/share/why3/theories/cursor.mlw
+libexec/spark/share/why3/theories/debug.mlw
+libexec/spark/share/why3/theories/exn.mlw
+libexec/spark/share/why3/theories/floating_point.mlw
+libexec/spark/share/why3/theories/fmap.mlw
+libexec/spark/share/why3/theories/for_drivers.mlw
+libexec/spark/share/why3/theories/function.mlw
+libexec/spark/share/why3/theories/graph.mlw
+libexec/spark/share/why3/theories/hashtbl.mlw
+libexec/spark/share/why3/theories/ieee_float.mlw
+libexec/spark/share/why3/theories/int.mlw
+libexec/spark/share/why3/theories/io.mlw
+libexec/spark/share/why3/theories/list.mlw
+libexec/spark/share/why3/theories/mach/array.mlw
+libexec/spark/share/why3/theories/mach/bv.mlw
+libexec/spark/share/why3/theories/mach/c.mlw
+libexec/spark/share/why3/theories/mach/float.mlw
+libexec/spark/share/why3/theories/mach/fxp.mlw
+libexec/spark/share/why3/theories/mach/int.mlw
+libexec/spark/share/why3/theories/mach/matrix.mlw
+libexec/spark/share/why3/theories/mach/onetime.mlw
+libexec/spark/share/why3/theories/mach/peano.mlw
+libexec/spark/share/why3/theories/mach/tagset.mlw
+libexec/spark/share/why3/theories/map.mlw
+libexec/spark/share/why3/theories/matrix.mlw
+libexec/spark/share/why3/theories/microc.mlw
+libexec/spark/share/why3/theories/null.mlw
+libexec/spark/share/why3/theories/number.mlw
+libexec/spark/share/why3/theories/ocaml.mlw
+libexec/spark/share/why3/theories/option.mlw
+libexec/spark/share/why3/theories/pigeon.mlw
+libexec/spark/share/why3/theories/pqueue.mlw
+libexec/spark/share/why3/theories/python.mlw
+libexec/spark/share/why3/theories/queue.mlw
+libexec/spark/share/why3/theories/random.mlw
+libexec/spark/share/why3/theories/real.mlw
+libexec/spark/share/why3/theories/ref.mlw
+libexec/spark/share/why3/theories/regexp.mlw
+libexec/spark/share/why3/theories/relations.mlw
+libexec/spark/share/why3/theories/seq.mlw
+libexec/spark/share/why3/theories/set.mlw
+libexec/spark/share/why3/theories/stack.mlw
+libexec/spark/share/why3/theories/string.mlw
+libexec/spark/share/why3/theories/tptp.mlw
+libexec/spark/share/why3/theories/tree.mlw
+libexec/spark/share/why3/theories/witness.mlw
+libexec/spark/share/why3/why3session.dtd
+share/spark/config/frames/config.xml
+share/spark/config/generated_menus.json
+share/spark/config/gnat2why/config.xml
+share/spark/config/gnatprove.conf
+share/spark/help.txt
+share/spark/runtimes/README
+share/spark/theories/_gnatprove_standard.mlw
+share/spark/theories/_gnatprove_standard_th.why
+share/spark/theories/ada__model.mlw
+share/spark/theories/ada__model_th.why
diff --git a/spark2014/buildlink3.mk b/spark2014/buildlink3.mk
new file mode 100644
index 0000000000..b4aae8d10c
--- /dev/null
+++ b/spark2014/buildlink3.mk
@@ -0,0 +1,17 @@
+# $NetBSD: buildlink3.mk,v 1.0 2024/05/06 11:00:00 dkazankov Exp $
+
+BUILDLINK_TREE+= spark2014
+
+.if !defined(SPARK2014_BUILDLINK3_MK)
+SPARK2014_BUILDLINK3_MK:=
+
+BUILDLINK_API_DEPENDS.spark2014+= spark2014>=13.0
+BUILDLINK_PKGSRCDIR.spark2014= ../../wip/spark2014
+BUILDLINK_DEPMETHOD.spark2014?= build
+
+BUILDLINK_FILES.spark2014= #empty
+BUILDLINK_CONTENTS_FILTER.spark2014= ${FALSE}
+
+.endif
+
+BUILDLINK_TREE+= -spark2014
diff --git a/spark2014/distinfo b/spark2014/distinfo
new file mode 100644
index 0000000000..00d3e97070
--- /dev/null
+++ b/spark2014/distinfo
@@ -0,0 +1,27 @@
+$NetBSD$
+
+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.2.0.tar.xz) = 89847ac474d00cde32fbcae20154f8aedff9c66158faf95ad7a78cc9a190d4c4
+SHA512 (gcc-13.2.0.tar.xz) = d99e4826a70db04504467e349e9fbaedaa5870766cda7c5cab50cdebedc4be755ebca5b789e1232a34a20be1a0b60097de9280efe47bdb71c73251e30b0862a2
+Size (gcc-13.2.0.tar.xz) = 87858592 bytes
+BLAKE2s (spark2014-13.0.0-12db22e854defa9d1c993ef904af1e72330a68ca.tar.gz) = 32b2081dfd7bbb4442bc791848cc4900a8cb9214e69fce6b55ef3724b2c9b145
+SHA512 (spark2014-13.0.0-12db22e854defa9d1c993ef904af1e72330a68ca.tar.gz) = 17644c49e642b2e79cfe481414d12df5b27bad003cdabbb0c9e88f5eb1f8b705b159791612a2d5f720e67017f0867ffaa5cfa0bc5fae8188442cd15fb456890b
+Size (spark2014-13.0.0-12db22e854defa9d1c993ef904af1e72330a68ca.tar.gz) = 11924977 bytes
+SHA1 (patch-Makefile) = 9157605f7a801b9a6efc91277610db77b5017b79
+SHA1 (patch-gnatprove.gpr) = 4fdad2117e0c5c68eb526fd9958ed3aad395ae9b
+SHA1 (patch-spark2014vsn.ads) = 602aa8c17a6cb67342ac09f3c88b7516b5af5ffb
+SHA1 (patch-src_common_platform.ads) = 4ff7b14c8811cecfa9fce51b813257c2e6a1efe1
+SHA1 (patch-src_common_x86__64-netbsd_platform.adb) = 44abca7d7c65a762e393cad9de0013d6949339e9
+SHA1 (patch-src_gnatprove_spark__report.adb) = ebea33ff633f24cee09188cbbded4b12deeaba1c
+SHA1 (patch-why3_Makefile.in) = 6172e55a5263ac19248916db57da4b7a387fdd7d
diff --git a/spark2014/patches/patch-Makefile b/spark2014/patches/patch-Makefile
new file mode 100644
index 0000000000..8a1ca7f268
--- /dev/null
+++ b/spark2014/patches/patch-Makefile
@@ -0,0 +1,66 @@
+$NetBSD: patch-Makefile,v 1.0 2024/05/13 10:30:00 dkazankov Exp $
+
+Fix install directory, build type, version number and NetBSD sha256sum
+
+--- Makefile.orig 2023-01-05 11:22:11.000000000 +0200
++++ Makefile 2024-05-20 14:53:45.799587834 +0300
+@@ -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=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.
diff --git a/spark2014/patches/patch-gnatprove.gpr b/spark2014/patches/patch-gnatprove.gpr
new file mode 100644
index 0000000000..d97f2ec49c
--- /dev/null
+++ b/spark2014/patches/patch-gnatprove.gpr
@@ -0,0 +1,27 @@
+$NetBSD: patch-gnatprove.gpr,v 1.0 2024/05/19 22:00:00 dkazankov Exp $
+
+Fix missing RELRO
+Add librt link on NetBSD
+
+--- gnatprove.gpr.orig 2023-01-05 11:22:11.000000000 +0200
++++ gnatprove.gpr 2024-05-20 16:33:06.170314454 +0300
+@@ -51,6 +51,8 @@
+ when "Production" =>
+ for Default_Switches ("Ada") use
+ Common_Switches & ("-O2", "-gnatn");
++ for PIC_Option ("Ada") use ("-fPIC");
++ for PIC_Option ("C") use ("-fPIC");
+ when "Coverage" =>
+ -- We don't do coverage of gnatprove yet, only gnat2why
+ null;
+@@ -61,6 +63,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 ("-lrt");
++ for Default_Switches ("C") use ("-lrt");
++ for Linker_Options use ("-lrt");
+ when others =>
+ null;
+ end case;
diff --git a/spark2014/patches/patch-spark2014vsn.ads b/spark2014/patches/patch-spark2014vsn.ads
new file mode 100644
index 0000000000..caac4355ef
--- /dev/null
+++ b/spark2014/patches/patch-spark2014vsn.ads
@@ -0,0 +1,15 @@
+$NetBSD: patch-spark2014vsn.ads,v 1.0 2024/05/19 22:00:00 dkazankov Exp $
+
+Fix version number
+
+--- spark2014vsn.ads.orig 2023-01-05 11:22:11.000000000 +0200
++++ spark2014vsn.ads 2024-05-19 23:19:54.364201126 +0300
+@@ -22,7 +22,7 @@
+
+ package SPARK2014VSN is
+
+- SPARK2014_Static_Version_String : constant String := "0.0w";
++ SPARK2014_Static_Version_String : constant String := "13.0";
+ -- Static string identifying this version, that can be used as an argument
+ -- to e.g. pragma Ident.
+ --
diff --git a/spark2014/patches/patch-src_common_platform.ads b/spark2014/patches/patch-src_common_platform.ads
new file mode 100644
index 0000000000..50e2a878cd
--- /dev/null
+++ b/spark2014/patches/patch-src_common_platform.ads
@@ -0,0 +1,15 @@
+$NetBSD: patch-src_common_platform.ads,v 1.0 2024/05/19 22:00:00 dkazankov Exp $
+
+Add NetBSD support
+
+--- src/common/platform.ads.orig 2023-01-05 11:22:11.000000000 +0200
++++ src/common/platform.ads 2024-05-19 22:23:47.685720387 +0300
+@@ -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;
+
diff --git a/spark2014/patches/patch-src_common_x86__64-netbsd_platform.adb b/spark2014/patches/patch-src_common_x86__64-netbsd_platform.adb
new file mode 100644
index 0000000000..cf339390b0
--- /dev/null
+++ b/spark2014/patches/patch-src_common_x86__64-netbsd_platform.adb
@@ -0,0 +1,44 @@
+$NetBSD: patch-src_common_x86__64-netbsd_platform.adb,v 1.0 2024/05/19 22:00:00 dkazankov Exp $
+
+Add NetBSD support
+
+--- /dev/null 2024-05-19 12:29:31.992878759 +0300
++++ src/common/x86_64-netbsd/platform.adb 2024-05-19 22:09:54.259989387 +0300
+@@ -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;
diff --git a/spark2014/patches/patch-src_gnatprove_spark__report.adb b/spark2014/patches/patch-src_gnatprove_spark__report.adb
new file mode 100644
index 0000000000..fbe0e8fc0b
--- /dev/null
+++ b/spark2014/patches/patch-src_gnatprove_spark__report.adb
@@ -0,0 +1,14 @@
+$NetBSD: patch-src_gnatprove_spark__report.adb,v 1.0 2024/05/19 22:00:00 dkazankov Exp $
+
+Add NetBSD support
+
+--- src/gnatprove/spark_report.adb.orig 2023-01-05 11:22:11.000000000 +0200
++++ src/gnatprove/spark_report.adb 2024-05-19 22:18:24.026147372 +0300
+@@ -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");
+
diff --git a/spark2014/patches/patch-why3_Makefile.in b/spark2014/patches/patch-why3_Makefile.in
new file mode 100644
index 0000000000..b39c0bb1fa
--- /dev/null
+++ b/spark2014/patches/patch-why3_Makefile.in
@@ -0,0 +1,15 @@
+$NetBSD: patch-why3_Makefile.in,v 1.0 2024/05/20 09:00:00 dkazankov Exp $
+
+NetBSD doesn't have -C option
+
+--- why3/Makefile.in.orig 2022-12-21 10:10:00.000000000 +0200
++++ why3/Makefile.in 2024-05-20 13:01:28.447738691 +0300
+@@ -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
+
diff --git a/spark2014/version.mk b/spark2014/version.mk
new file mode 100644
index 0000000000..5daa83a961
--- /dev/null
+++ b/spark2014/version.mk
@@ -0,0 +1,3 @@
+# $NetBSD: version.mk,v 1.2 2024/05/02 14:00:00 dkazankov Exp $
+
+SPARK2014_VERSION:= 13.0.0
Home |
Main Index |
Thread Index |
Old Index