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: Mon Jul 28 07:00:55 UTC 2025
Modified Files:
pkgsrc/lang: Makefile
Added Files:
pkgsrc/lang/spark2014-14: DESCR Makefile PLIST distinfo
pkgsrc/lang/spark2014-14/patches: patch-Makefile
patch-Makefile.gnatprove patch-gnat2why_Makefile
patch-gnatprove.gpr patch-src_common_platform.ads
patch-src_common_semaphores__c.c
patch-src_common_x86__64-netbsd_platform.adb
patch-src_gnatprove_configuration.adb
patch-src_gnatprove_spark__report.adb
Log Message:
lang/spark2014-14: add new package 14.2.0
SPARK 2014 toolset, FSF release 14
To generate a diff of this commit:
cvs rdiff -u -r1.766 -r1.767 pkgsrc/lang/Makefile
cvs rdiff -u -r0 -r1.1 pkgsrc/lang/spark2014-14/DESCR \
pkgsrc/lang/spark2014-14/Makefile pkgsrc/lang/spark2014-14/PLIST \
pkgsrc/lang/spark2014-14/distinfo
cvs rdiff -u -r0 -r1.1 pkgsrc/lang/spark2014-14/patches/patch-Makefile \
pkgsrc/lang/spark2014-14/patches/patch-Makefile.gnatprove \
pkgsrc/lang/spark2014-14/patches/patch-gnat2why_Makefile \
pkgsrc/lang/spark2014-14/patches/patch-gnatprove.gpr \
pkgsrc/lang/spark2014-14/patches/patch-src_common_platform.ads \
pkgsrc/lang/spark2014-14/patches/patch-src_common_semaphores__c.c \
pkgsrc/lang/spark2014-14/patches/patch-src_common_x86__64-netbsd_platform.adb \
pkgsrc/lang/spark2014-14/patches/patch-src_gnatprove_configuration.adb \
pkgsrc/lang/spark2014-14/patches/patch-src_gnatprove_spark__report.adb
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.766 pkgsrc/lang/Makefile:1.767
--- pkgsrc/lang/Makefile:1.766 Sun Jul 27 09:17:17 2025
+++ pkgsrc/lang/Makefile Mon Jul 28 07:00:55 2025
@@ -1,4 +1,4 @@
-# $NetBSD: Makefile,v 1.766 2025/07/27 09:17:17 wiz Exp $
+# $NetBSD: Makefile,v 1.767 2025/07/28 07:00:55 dkazankov Exp $
#
COMMENT= Programming languages
@@ -339,6 +339,7 @@ SUBDIR+= smlnj
SUBDIR+= snobol
SUBDIR+= spago
SUBDIR+= spark2014-13
+SUBDIR+= spark2014-14
SUBDIR+= spidermonkey
SUBDIR+= spidermonkey185
SUBDIR+= spl
Added files:
Index: pkgsrc/lang/spark2014-14/DESCR
diff -u /dev/null pkgsrc/lang/spark2014-14/DESCR:1.1
--- /dev/null Mon Jul 28 07:00:55 2025
+++ pkgsrc/lang/spark2014-14/DESCR Mon Jul 28 07:00:55 2025
@@ -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.
Index: pkgsrc/lang/spark2014-14/Makefile
diff -u /dev/null pkgsrc/lang/spark2014-14/Makefile:1.1
--- /dev/null Mon Jul 28 07:00:55 2025
+++ pkgsrc/lang/spark2014-14/Makefile Mon Jul 28 07:00:55 2025
@@ -0,0 +1,144 @@
+# $NetBSD: Makefile,v 1.1 2025/07/28 07:00:55 dkazankov Exp $
+
+DISTNAME= ${GITHUB_PROJECT}-fsf-14
+PKGNAME= ${GITHUB_PROJECT}-14-14.2.0
+CATEGORIES= lang devel
+MASTER_SITES= ${MASTER_SITE_GITHUB:=AdaCore/}
+GITHUB_PROJECT= spark2014
+GITHUB_TAG= fsf-14
+DISTFILES= ${DEFAULT_DISTFILES}
+
+MAINTAINER= dkazankov%NetBSD.org@localhost
+HOMEPAGE= https://github.com/AdaCore/spark2014
+COMMENT= SPARK 2014 toolset, FSF release 14
+LICENSE= gnu-gpl-v3
+
+USE_LANGUAGES= c ada
+
+USE_TOOLS+= gmake
+
+HAS_CONFIGURE= yes
+
+CHECK_PIE_SKIP+= gcc14-gnat/bin/*
+
+GITHUB_SUBMODULES+= AdaCore why3 fb4ca6cd8c7d888d3e8d281e6de87c66ec20f084 why3
+
+# Do not use GNAT 14.3 sources
+GCC_DISTNAME= gcc-${PKGVERSION_NOREV}
+GCC_EXTRACT_SUFFIX= .tar.xz
+GCC_DISTFILE= ${GCC_DISTNAME}${GCC_EXTRACT_SUFFIX}
+
+DISTFILES+= ${GCC_DISTFILE}
+MASTER_SITES+= ${MASTER_SITE_GNU:=gcc/${GCC_DISTNAME}/}
+
+.include "../../mk/bsd.prefs.mk"
+
+GCC_REQD+= 14
+
+CONFIG_SHELL= ${MAKE_PROGRAM}
+CONFIGURE_ARGS+= DESTDIR=${DESTDIR} PREFIX=${PREFIX}/gcc14-gnat
+CONFIGURE_SCRIPT= setup
+
+MAKE_FLAGS+= DESTDIR=${DESTDIR} PREFIX=${PREFIX}/gcc14-gnat
+
+INSTALL_TARGET= install-all
+
+SUBST_CLASSES+= version
+SUBST_MESSAGE.version= Replace version in ${SUBST_FILES.version}
+SUBST_STAGE.version= pre-configure
+SUBST_FILES.version= Makefile spark2014vsn.ads
+SUBST_SED.version= -e "s,0.0w,FSF 14.0,"
+
+.if ${OPSYS} == "NetBSD"
+SUBST_CLASSES+= sha256
+SUBST_MESSAGE.sha256= Replace sha256sum in ${SUBST_FILES.sha256}
+SUBST_STAGE.sha256= pre-configure
+SUBST_FILES.sha256= Makefile
+SUBST_SED.sha256= -e "s,sha256sum,sha256 -n,"
+
+SUBST_CLASSES+= install
+SUBST_MESSAGE.install= Remove -C in ${SUBST_FILES.install}
+SUBST_STAGE.install= pre-configure
+SUBST_FILES.install= why3/Makefile.in
+SUBST_SED.install= -e "s,do install -C,do install,"
+
+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'
+.endif
+
+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} gcc14-gnat \( -type f -or -type l \) -print | ${SORT};
+
+#BUILDLINK_DEPMETHOD.sparklib-14= full
+#.include "../../devel/ada-sparklib-14/buildlink3.mk"
+
+.include "../../devel/gprbuild/buildlink3.mk"
+
+.include "../../textproc/ada-xmlada-25/buildlink3.mk"
+.include "../../math/ada-adasat-25/buildlink3.mk"
+.include "../../devel/ada-libgpr-25/buildlink3.mk"
+.include "../../devel/ada-gnatcoll-core-25/buildlink3.mk"
+.include "../../devel/ada-gnatcoll-bindings-25/buildlink3.mk"
+.include "../../devel/ada-libgpr2-25/buildlink3.mk"
+
+.include "../../lang/python/tool.mk"
+
+OCAML_SRC= ${WRKSRC}/why3
+
+BUILDLINK_DEPMETHOD.ocaml= build
+.include "../../lang/ocaml/ocaml.mk"
+
+BUILDLINK_DEPMETHOD.menhir= build
+.include "../../devel/menhir/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml-num= build
+.include "../../math/ocaml-num/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocamlgraph= build
+.include "../../devel/ocamlgraph/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml-re= build
+.include "../../devel/ocaml-re/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml-seq= build
+.include "../../devel/ocaml-seq/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml-yojson= build
+.include "../../devel/ocaml-yojson/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml-zarith= build
+.include "../../math/ocaml-zarith/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml-sexplib= build
+.include "../../devel/ocaml-sexplib/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml-ppx_sexp_conv= build
+.include "../../devel/ocaml-ppx_sexp_conv/buildlink3.mk"
+BUILDLINK_DEPMETHOD.ocaml-ppx_deriving= build
+.include "../../devel/ocaml-ppx_deriving/buildlink3.mk"
+
+#BUILDLINK_DEPMETHOD.ocaml-base= build
+#.include "../../devel/ocaml-base/buildlink3.mk"
+#BUILDLINK_DEPMETHOD.ocaml-sexplib0= build
+#.include "../../devel/ocaml-sexplib0/buildlink3.mk"
+#BUILDLINK_DEPMETHOD.ocaml-parsexp= build
+#.include "../../devel/ocaml-parsexp/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"
+
+# libgpr2 dependencies
+.include "../../devel/gmp/buildlink3.mk"
+USE_GNU_ICONV= yes
+.include "../../converters/libiconv/buildlink3.mk"
+
+.include "../../mk/pthread.buildlink3.mk"
+
+.include "../../mk/bsd.pkg.mk"
Index: pkgsrc/lang/spark2014-14/PLIST
diff -u /dev/null pkgsrc/lang/spark2014-14/PLIST:1.1
--- /dev/null Mon Jul 28 07:00:55 2025
+++ pkgsrc/lang/spark2014-14/PLIST Mon Jul 28 07:00:55 2025
@@ -0,0 +1,340 @@
+@comment $NetBSD: PLIST,v 1.1 2025/07/28 07:00:55 dkazankov Exp $
+gcc14-gnat/bin/gnat2why
+gcc14-gnat/bin/gnatprove
+gcc14-gnat/bin/spark_memcached_wrapper
+gcc14-gnat/bin/spark_report
+gcc14-gnat/bin/spark_semaphore_wrapper
+gcc14-gnat/bin/target.atp
+gcc14-gnat/libexec/spark/bin/fake_alt-ergo
+gcc14-gnat/libexec/spark/bin/fake_cvc4
+gcc14-gnat/libexec/spark/bin/fake_cvc5
+gcc14-gnat/libexec/spark/bin/fake_z3
+gcc14-gnat/libexec/spark/bin/gnatwhy3
+gcc14-gnat/libexec/spark/bin/gnatwhy3.hash
+gcc14-gnat/libexec/spark/bin/why3
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/bin/why3config.cmxs
+gcc14-gnat/libexec/spark/bin/why3cpulimit
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/bin/why3realize.cmxs
+gcc14-gnat/libexec/spark/bin/why3server
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/bin/why3session.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/commands/why3config.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/commands/why3doc.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/commands/why3execute.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/commands/why3extract.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/commands/why3pp.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/commands/why3prove.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/commands/why3realize.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/commands/why3replay.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/commands/why3session.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/commands/why3shell.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/commands/why3show.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/commands/why3wc.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/commands/why3webserver.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/plugins/ada_terms.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/plugins/cfg.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/plugins/dimacs.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/plugins/genequlin.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/plugins/gnat_json.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/plugins/microc.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/plugins/python.cmxs
+${PLIST.ocaml-opt}gcc14-gnat/libexec/spark/lib/why3/plugins/tptp.cmxs
+gcc14-gnat/libexec/spark/lib/why3/why3-call-pvs
+gcc14-gnat/libexec/spark/lib/why3/why3cpulimit
+gcc14-gnat/libexec/spark/lib/why3/why3server
+gcc14-gnat/libexec/spark/share/why3/drivers/alt-ergo_gnatprove.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/alt_ergo.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/alt_ergo_2_2_0.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/alt_ergo_2_3.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/alt_ergo_common.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/alt_ergo_fp.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/alt_ergo_model.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/alt_ergo_smt2.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/beagle.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/colibri.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/colibri2.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/coq-common.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/coq-realizations.aux
+gcc14-gnat/libexec/spark/share/why3/drivers/coq-realize.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/coq-ssreflect.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/coq.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/coq_gnatprove.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc3.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc4-realize.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc4.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc4_14.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc4_15.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc4_15_counterexample.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc4_16.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc4_16.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc4_16_counterexample.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc4_17.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc4_17_counterexample.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc4_18_strings.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc4_18_strings_counterexample.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc4_bv.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc5.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc5_counterexample.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc5_gnatprove.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc5_gnatprove_ce.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc5_strings.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/cvc5_strings_counterexample.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/discrimination.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/dreal.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/eprover.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/gappa.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/iprover.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/isabelle-common.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/isabelle-realizations.aux
+gcc14-gnat/libexec/spark/share/why3/drivers/isabelle-realize.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/isabelle.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/mathematica.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/mathsat.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/metis.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/metitarski.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/no-bv.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/polypaver.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/princess.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/psyche.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/pvs-common.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/pvs-realizations.aux
+gcc14-gnat/libexec/spark/share/why3/drivers/pvs-realize.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/pvs.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/safeprover.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/simplify.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/smt-libv2-bv-realization.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/smt-libv2-bv.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/smt-libv2-floats-gnatprove.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/smt-libv2-floats-int_via_bv.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/smt-libv2-floats-int_via_real.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/smt-libv2-floats.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/smt-libv2-gnatprove.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/smt-libv2.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/smtlib-strings.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/spass.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/spass_types.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/tptp-tff0.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/tptp-tff1.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/tptp.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/vampire.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/vampire_4_2_2.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/vampire_4_5_1.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/verit.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/why3.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/why3_smt.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/why3_tptp.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/yices-smt2.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/yices.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/z3.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/z3_432.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/z3_440.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/z3_440_counterexample.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/z3_471.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/z3_471_counterexample.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/z3_471_nobv.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/z3_487.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/z3_487_counterexample.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/z3_bv.gen
+gcc14-gnat/libexec/spark/share/why3/drivers/z3_gnatprove.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/z3_gnatprove_ce.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/z3_no_quant.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/z3_smtv1.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/zenon.drv
+gcc14-gnat/libexec/spark/share/why3/drivers/zenon_modulo.drv
+gcc14-gnat/libexec/spark/share/why3/images/fatcow.rc
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/accept.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/bin.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/bomb.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/brick_delete.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/bullet_black.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/bullet_blue.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/bullet_green.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/bullet_red.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/bullet_white.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/cancel.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/control_pause_blue.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/control_play_blue.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/database_delete.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/ddr_memory.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/delete.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/exclamation.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/folder.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/help.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/magic_wand_2.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/multitool.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/package.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/pencil.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/readme-fatcow.txt
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/script.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/time_delete.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/timeline.png
+gcc14-gnat/libexec/spark/share/why3/images/fatcow/update.png
+gcc14-gnat/libexec/spark/share/why3/images/logo-why.png
+gcc14-gnat/libexec/spark/share/why3/lang/why3.lang
+gcc14-gnat/libexec/spark/share/why3/lang/why3c.lang
+gcc14-gnat/libexec/spark/share/why3/lang/why3py.lang
+gcc14-gnat/libexec/spark/share/why3/libs/coq/BuiltIn.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/HighOrd.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/SPARK.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/WellFounded.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/_CoqProject
+gcc14-gnat/libexec/spark/share/why3/libs/coq/bool/Bool.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/bv/BV_Gen.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/bv/Pow2int.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/floating_point/Double.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/floating_point/DoubleFormat.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/floating_point/GenFloat.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/floating_point/Rounding.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/floating_point/Single.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/floating_point/SingleFormat.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/for_drivers/ComputerOfEuclideanDivision.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/ieee_float/Float32.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/ieee_float/Float64.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/ieee_float/GenericFloat.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/ieee_float/RoundingMode.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/int/Abs.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/int/ComputerDivision.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/int/Div2.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/int/EuclideanDivision.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/int/Exponentiation.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/int/Int.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/int/MinMax.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/int/NumOf.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/int/Power.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/Append.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/Combine.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/Distinct.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/HdTl.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/HdTlNoOpt.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/Length.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/List.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/Mem.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/Nth.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/NthHdTl.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/NthLength.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/NthLengthAppend.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/NthNoOpt.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/NumOcc.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/Permut.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/RevAppend.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/list/Reverse.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/map/Const.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/map/Map.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/map/MapInjection.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/map/MapPermut.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/map/Occ.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/number/Coprime.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/number/Divisibility.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/number/Gcd.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/number/Parity.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/number/Prime.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/option/Option.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/real/Abs.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/real/ExpLog.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/real/FromInt.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/real/MinMax.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/real/PowerInt.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/real/PowerReal.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/real/Real.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/real/RealInfix.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/real/Square.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/real/Trigonometry.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/real/Truncate.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/set/Cardinal.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/set/Fset.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/set/FsetInduction.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/set/FsetInt.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/set/FsetSum.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/set/Set.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/set/SetApp.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/set/SetAppInt.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/set/SetImp.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/set/SetImpInt.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/spark/SPARK_Integer_Arithmetic.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/spark/SPARK_Raising_Order.v
+gcc14-gnat/libexec/spark/share/why3/libs/coq/version
+gcc14-gnat/libexec/spark/share/why3/libs/coq/version.in
+gcc14-gnat/libexec/spark/share/why3/provers-detection-data.conf
+gcc14-gnat/libexec/spark/share/why3/theories/algebra.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/array.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/bag.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/bintree.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/bool.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/bv.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/byte_string.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/cursor.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/debug.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/exn.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/floating_point.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/fmap.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/for_drivers.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/function.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/graph.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/hashtbl.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/ieee_float.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/int.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/io.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/list.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/mach/array.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/mach/bv.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/mach/c.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/mach/float.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/mach/fxp.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/mach/int.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/mach/matrix.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/mach/onetime.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/mach/peano.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/mach/tagset.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/map.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/matrix.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/microc.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/null.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/number.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/ocaml.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/option.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/pigeon.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/pqueue.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/python.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/queue.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/random.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/real.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/ref.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/regexp.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/relations.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/seq.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/set.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/stack.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/string.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/tptp.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/tree.mlw
+gcc14-gnat/libexec/spark/share/why3/theories/witness.mlw
+gcc14-gnat/libexec/spark/share/why3/why3session.dtd
+gcc14-gnat/share/spark/config/frames/config.xml
+gcc14-gnat/share/spark/config/gnat2why/config.xml
+gcc14-gnat/share/spark/config/gnatprove.conf
+gcc14-gnat/share/spark/explain_codes/E0001.md
+gcc14-gnat/share/spark/explain_codes/E0002.md
+gcc14-gnat/share/spark/explain_codes/E0003.md
+gcc14-gnat/share/spark/explain_codes/E0004.md
+gcc14-gnat/share/spark/explain_codes/E0005.md
+gcc14-gnat/share/spark/explain_codes/E0006.md
+gcc14-gnat/share/spark/explain_codes/E0007.md
+gcc14-gnat/share/spark/explain_codes/E0008.md
+gcc14-gnat/share/spark/explain_codes/E0009.md
+gcc14-gnat/share/spark/explain_codes/E0010.md
+gcc14-gnat/share/spark/explain_codes/E0011.md
+gcc14-gnat/share/spark/explain_codes/E0012.md
+gcc14-gnat/share/spark/explain_codes/E0013.md
+gcc14-gnat/share/spark/explain_codes/E0014.md
+gcc14-gnat/share/spark/explain_codes/E0015.md
+gcc14-gnat/share/spark/explain_codes/E0016.md
+gcc14-gnat/share/spark/explain_codes/E0017.md
+gcc14-gnat/share/spark/explain_codes/E0018.md
+gcc14-gnat/share/spark/explain_codes/README.md
+gcc14-gnat/share/spark/help.txt
+gcc14-gnat/share/spark/runtimes/README
+gcc14-gnat/share/spark/theories/_gnatprove_standard.mlw
+gcc14-gnat/share/spark/theories/_gnatprove_standard_th.why
+gcc14-gnat/share/spark/theories/ada__model.mlw
+gcc14-gnat/share/spark/theories/ada__model_th.why
+@pkgdir gcc14-gnat/lib/gnat
+@pkgdir gcc14-gnat/include/spark
Index: pkgsrc/lang/spark2014-14/distinfo
diff -u /dev/null pkgsrc/lang/spark2014-14/distinfo:1.1
--- /dev/null Mon Jul 28 07:00:55 2025
+++ pkgsrc/lang/spark2014-14/distinfo Mon Jul 28 07:00:55 2025
@@ -0,0 +1,20 @@
+$NetBSD: distinfo,v 1.1 2025/07/28 07:00:55 dkazankov Exp $
+
+BLAKE2s (AdaCore-why3-fb4ca6cd8c7d888d3e8d281e6de87c66ec20f084.tar.gz) = c35a6eaceeceef43b60f671d2e0fb9953f4e0960465175b68cee7e76c197ab0e
+SHA512 (AdaCore-why3-fb4ca6cd8c7d888d3e8d281e6de87c66ec20f084.tar.gz) =
88220595eae9c5cf4125c0dc9d5176e637a1f1e355f61f51176bdb7643a000c837e501101e45c2b50ae3f41f81436e1133be241fd5fb0b6816823b2106113ae7
+Size (AdaCore-why3-fb4ca6cd8c7d888d3e8d281e6de87c66ec20f084.tar.gz) = 7119379 bytes
+BLAKE2s (gcc-14.2.0.tar.xz) = 4cbc121d8d3982be05e1d0621363c6ec4cd34c78007a1af0599559370a93376e
+SHA512 (gcc-14.2.0.tar.xz) = 932bdef0cda94bacedf452ab17f103c0cb511ff2cec55e9112fc0328cbf1d803b42595728ea7b200e0a057c03e85626f937012e49a7515bc5dd256b2bf4bc396
+Size (gcc-14.2.0.tar.xz) = 92306460 bytes
+BLAKE2s (spark2014-fsf-14.tar.gz) = dea834098ecb4ff6cdbff3c5617268161c0deacb3a344d6f3dac9948971f098e
+SHA512 (spark2014-fsf-14.tar.gz) = 73e4aba26f1065a56732ef7b0957dc0d77f5dd176d80f46676f1568ce2bd38d3fc5178984d6f77fe504152ce6f8c1f4496e852e14b88a3c770fe1eb558d6dbd5
+Size (spark2014-fsf-14.tar.gz) = 12097762 bytes
+SHA1 (patch-Makefile) = 3fcafecc8294ac9613e370b601ae866edd2efaea
+SHA1 (patch-Makefile.gnatprove) = 6a171f122521d476af60fa06158bbbb14d35953f
+SHA1 (patch-gnat2why_Makefile) = e36928457e9637956297f77f3886941d98ccbcc3
+SHA1 (patch-gnatprove.gpr) = 4960d85bd25956316b918c7b0d0666864fb7538c
+SHA1 (patch-src_common_platform.ads) = 720a3f7e882cfe1b97c852428d7bbd9a489833cd
+SHA1 (patch-src_common_semaphores__c.c) = 1aced175f2a6e36bcc48868de399d76e65a6079f
+SHA1 (patch-src_common_x86__64-netbsd_platform.adb) = bf08dc93c7bb2348b5251a33e111690e0c87580e
+SHA1 (patch-src_gnatprove_configuration.adb) = 336b9df5987daa688e0c694a3e0069a516d46edf
+SHA1 (patch-src_gnatprove_spark__report.adb) = 50f27b460b5ceefb97b7f78e56b3fd1c5e73f159
Index: pkgsrc/lang/spark2014-14/patches/patch-Makefile
diff -u /dev/null pkgsrc/lang/spark2014-14/patches/patch-Makefile:1.1
--- /dev/null Mon Jul 28 07:00:55 2025
+++ pkgsrc/lang/spark2014-14/patches/patch-Makefile Mon Jul 28 07:00:55 2025
@@ -0,0 +1,78 @@
+$NetBSD: patch-Makefile,v 1.1 2025/07/28 07:00:55 dkazankov Exp $
+
+Fix install directory
+Fix version value substitution
+Fix build type
+Remove unused SPARKlib build
+
+--- Makefile.orig 2024-01-11 17:55:20.000000000 +0200
++++ Makefile
+@@ -43,7 +43,9 @@
+
+ COVERAGE_ROOT_DIR=/it/wave/x86_64-linux/spark2014-core_assertions_coverage/src/
+
+-INSTALLDIR=$(CURDIR)/install
++PREFIX=
++DESTDIR=
++INSTALLDIR=$(DESTDIR)$(PREFIX)
+ SHAREDIR=$(INSTALLDIR)/share
+ SIDDIR=$(SHAREDIR)/gnat2why-sids
+ INCLUDEDIR=$(INSTALLDIR)/include/spark
+@@ -81,7 +83,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 --disable-coq-libs
+
+@@ -100,26 +102,22 @@
+ $(EXPLAINCODESDIR) $(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/explain_codes/* $(EXPLAINCODESDIR)
+ $(CP) share/spark/theories/*why $(THEORIESDIR)
+ $(CP) share/spark/theories/*mlw $(THEORIESDIR)
+ $(CP) share/spark/runtimes/README $(RUNTIMESDIR)
+- @echo "Generate Coq files by preprocessing context files:"
+- $(MAKE) -C include generate
+- $(CP) include/src/*.ad? $(INCLUDEDIR)
+- $(CP) include/*.gpr $(LIBDIR)
+- $(CP) include/proof $(LIBDIR)
+
+ doc: $(DOC)
+
+ doc-nightly: $(DOC)
+- cd docs/ug; $(MAKE) generate-nightly VERSION=$(VERSION)
++ cd docs/ug; $(MAKE) generate-nightly VERSION="$(VERSION)"
+
+ $(DOC):
+- $(MAKE) -C docs/$@ latexpdf LATEXOPTS="-interaction=nonstopmode" VERSION=$(VERSION)
+- $(MAKE) -C docs/$@ html VERSION=$(VERSION)
++ $(MAKE) -C docs/$@ latexpdf LATEXOPTS="-interaction=nonstopmode" VERSION="$(VERSION)"
++ $(MAKE) -C docs/$@ html VERSION="$(VERSION)"
+ mkdir -p $(DOCDIR)/pdf
+ mkdir -p $(DOCDIR)/html/$@
+ $(CP) docs/$@/_build/latex/*.pdf $(DOCDIR)/pdf
+@@ -134,7 +132,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=$(PROD)
+ # (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.
+@@ -181,7 +179,7 @@
+ fi
+
+ gnatprove:
+- $(MAKE) -f Makefile.gnatprove build
++ $(MAKE) -f Makefile.gnatprove build PROD=$(PROD)
+
+ gnatprove-nightly:
+ $(MAKE) -f Makefile.gnatprove build PROD=$(PROD)
Index: pkgsrc/lang/spark2014-14/patches/patch-Makefile.gnatprove
diff -u /dev/null pkgsrc/lang/spark2014-14/patches/patch-Makefile.gnatprove:1.1
--- /dev/null Mon Jul 28 07:00:55 2025
+++ pkgsrc/lang/spark2014-14/patches/patch-Makefile.gnatprove Mon Jul 28 07:00:55 2025
@@ -0,0 +1,20 @@
+$NetBSD: patch-Makefile.gnatprove,v 1.1 2025/07/28 07:00:55 dkazankov Exp $
+
+Add options for gprbuild
+
+--- Makefile.gnatprove.orig 2024-01-11 17:55:20.000000000 +0200
++++ Makefile.gnatprove
+@@ -1,11 +1,12 @@
+ # need to define this variable here, to allow overriding it when calling the
+ # Makefile
+ PROD=
++GPRBUILD_OPTIONS=
+
+ all: build
+
+ build:
+- gprbuild -p -j0 -P gnatprove.gpr $(PROD)
++ gprbuild -p -j0 -P gnatprove.gpr $(PROD) $(GPRBUILD_OPTIONS)
+
+ codepeer-run:
+ gnatsas analyze -P gnatprove.gpr --no-gnat
Index: pkgsrc/lang/spark2014-14/patches/patch-gnat2why_Makefile
diff -u /dev/null pkgsrc/lang/spark2014-14/patches/patch-gnat2why_Makefile:1.1
--- /dev/null Mon Jul 28 07:00:55 2025
+++ pkgsrc/lang/spark2014-14/patches/patch-gnat2why_Makefile Mon Jul 28 07:00:55 2025
@@ -0,0 +1,23 @@
+$NetBSD: patch-gnat2why_Makefile,v 1.1 2025/07/28 07:00:55 dkazankov Exp $
+
+Make gprbuild options settable
+
+--- gnat2why/Makefile.orig 2024-01-11 17:55:20.000000000 +0200
++++ gnat2why/Makefile
+@@ -2,6 +2,7 @@
+ # This makefile assumes that it executed from the backend directory.
+
+ GPRBUILD=gprbuild
++GPRBUILD_OPTIONS=-j$(PROCS) -cargs $(CFLAGS) -largs $(LDFLAGS)
+
+ # number of processors
+ PROCS=0
+@@ -72,7 +73,7 @@
+ mv $(GEN_IL_FILES) ../obj
+
+ build: setup force
+- $(GPRBUILD) $(GPRARGS) $(COVERAGEARGS) -Pgnat2why -j$(PROCS) -cargs ${CFLAGS} -largs $(LDFLAGS)
++ $(GPRBUILD) $(GPRARGS) $(COVERAGEARGS) -Pgnat2why $(GPRBUILD_OPTIONS)
+
+ # Compilation and linking settings for coverage and profiling; for details see
+ # "Code Coverage and Profiling" in GNAT User's Guide.
Index: pkgsrc/lang/spark2014-14/patches/patch-gnatprove.gpr
diff -u /dev/null pkgsrc/lang/spark2014-14/patches/patch-gnatprove.gpr:1.1
--- /dev/null Mon Jul 28 07:00:55 2025
+++ pkgsrc/lang/spark2014-14/patches/patch-gnatprove.gpr Mon Jul 28 07:00:55 2025
@@ -0,0 +1,27 @@
+$NetBSD: patch-gnatprove.gpr,v 1.1 2025/07/28 07:00:55 dkazankov Exp $
+
+Fix missing RELRO
+Add librt link on NetBSD
+
+--- gnatprove.gpr.orig 2023-01-05 11:22:11.000000000 +0200
++++ gnatprove.gpr
+@@ -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;
Index: pkgsrc/lang/spark2014-14/patches/patch-src_common_platform.ads
diff -u /dev/null pkgsrc/lang/spark2014-14/patches/patch-src_common_platform.ads:1.1
--- /dev/null Mon Jul 28 07:00:55 2025
+++ pkgsrc/lang/spark2014-14/patches/patch-src_common_platform.ads Mon Jul 28 07:00:55 2025
@@ -0,0 +1,16 @@
+$NetBSD: patch-src_common_platform.ads,v 1.1 2025/07/28 07:00:55 dkazankov Exp $
+
+Add NetBSD support
+
+--- src/common/platform.ads.orig 2024-01-11 17:55:20.000000000 +0200
++++ src/common/platform.ads
+@@ -30,7 +30,8 @@
+
+ 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, AArch64_Linux);
++ X86_64_FreeBSD, CodePeer_OS, AArch64_Darwin, AArch64_Linux,
++ X86_64_NetBSD);
+
+ function Get_OS_Flavor return Host_Operating_System_Flavor;
+
Index: pkgsrc/lang/spark2014-14/patches/patch-src_common_semaphores__c.c
diff -u /dev/null pkgsrc/lang/spark2014-14/patches/patch-src_common_semaphores__c.c:1.1
--- /dev/null Mon Jul 28 07:00:55 2025
+++ pkgsrc/lang/spark2014-14/patches/patch-src_common_semaphores__c.c Mon Jul 28 07:00:55 2025
@@ -0,0 +1,75 @@
+$NetBSD: patch-src_common_semaphores__c.c,v 1.1 2025/07/28 07:00:55 dkazankov Exp $
+
+Fix runtime error caused semaphore names on NetBSD
+
+--- src/common/semaphores_c.c.orig 2024-01-11 17:55:20.000000000 +0200
++++ src/common/semaphores_c.c
+@@ -30,8 +30,35 @@
+ #include <stdio.h>
+ #include <stdlib.h>
+
++#if defined (__NetBSD__)
++#include <string.h>
++
++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 +67,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 +105,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-14/patches/patch-src_common_x86__64-netbsd_platform.adb
diff -u /dev/null pkgsrc/lang/spark2014-14/patches/patch-src_common_x86__64-netbsd_platform.adb:1.1
--- /dev/null Mon Jul 28 07:00:55 2025
+++ pkgsrc/lang/spark2014-14/patches/patch-src_common_x86__64-netbsd_platform.adb Mon Jul 28 07:00:55 2025
@@ -0,0 +1,44 @@
+$NetBSD: patch-src_common_x86__64-netbsd_platform.adb,v 1.1 2025/07/28 07:00:55 dkazankov Exp $
+
+Add NetBSD support
+
+--- /dev/null
++++ 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;
Index: pkgsrc/lang/spark2014-14/patches/patch-src_gnatprove_configuration.adb
diff -u /dev/null pkgsrc/lang/spark2014-14/patches/patch-src_gnatprove_configuration.adb:1.1
--- /dev/null Mon Jul 28 07:00:55 2025
+++ pkgsrc/lang/spark2014-14/patches/patch-src_gnatprove_configuration.adb Mon Jul 28 07:00:55 2025
@@ -0,0 +1,58 @@
+$NetBSD: patch-src_gnatprove_configuration.adb,v 1.1 2025/07/28 07:00:55 dkazankov Exp $
+
+Adjust gnatprove to changes in gpr2 API
+The new API simplifies the tree load function, and error reporting.
+This requires this change to gnatprove.
+https://github.com/AdaCore/spark2014/commit/1567db99c5785a722cb7601e406c486b680c1fd7
+
+Fix compilation error
+The function Visible_Source already returns a Source object
+https://github.com/AdaCore/spark2014/commit/42ee20a76b74120fb78a83b3f0e2647803b469b9
+
+--- src/gnatprove/configuration.adb.orig 2024-01-11 17:55:20.000000000 +0200
++++ src/gnatprove/configuration.adb
+@@ -1466,11 +1466,14 @@
+ Status : Boolean;
+ begin
+ Proj_Opt.Add_Switch (Options.P, Project_File);
+- Proj_Opt.Finalize;
+- Status := Proj_Opt.Load_Project (Tree);
++
++ -- Do not display warnings, as those messages will be duplicated
++ -- during the call to gprbuild.
++ GPR2.Project.Tree.Verbosity := GPR2.Project.Tree.Errors;
++
++ Status := Tree.Load (Proj_Opt, Absent_Dir_Error => GPR2.No_Error);
++
+ if not Status then
+- GPR2.Log.Output_Messages
+- (Tree.Log_Messages.all, Information => False);
+ Fail ("");
+ end if;
+
+@@ -1482,8 +1485,13 @@
+ declare
+ Msgs : GPR2.Log.Object;
+ begin
+- Tree.Update_Sources (Messages => Msgs);
+- GPR2.Log.Output_Messages (Msgs, Information => False);
++ -- When updating the sources we now need both warnings and
++ -- errors, in particular since duplicated body situation is
++ -- a warning.
++
++ GPR2.Project.Tree.Verbosity :=
++ GPR2.Project.Tree.Warnings_And_Errors;
++ Tree.Update_Sources (Msgs);
+ end;
+ end if;
+ end;
+@@ -2588,8 +2596,7 @@
+ then
+ CU := View_DB.Compilation_Unit (Elt);
+ elsif View_DB.Source_Option > No_Source then
+- VS :=
+- View_DB.Visible_Source (GPR2.Simple_Name (Elt)).Source;
++ VS := View_DB.Visible_Source (GPR2.Simple_Name (Elt));
+ if VS.Is_Defined
+ and then View_DB.Has_Compilation_Unit (VS.Unit.Name)
+ then
Index: pkgsrc/lang/spark2014-14/patches/patch-src_gnatprove_spark__report.adb
diff -u /dev/null pkgsrc/lang/spark2014-14/patches/patch-src_gnatprove_spark__report.adb:1.1
--- /dev/null Mon Jul 28 07:00:55 2025
+++ pkgsrc/lang/spark2014-14/patches/patch-src_gnatprove_spark__report.adb Mon Jul 28 07:00:55 2025
@@ -0,0 +1,14 @@
+$NetBSD: patch-src_gnatprove_spark__report.adb,v 1.1 2025/07/28 07:00:55 dkazankov Exp $
+
+Add NetBSD support
+
+--- src/gnatprove/spark_report.adb.orig 2024-01-11 17:55:20.000000000 +0200
++++ src/gnatprove/spark_report.adb
+@@ -1110,6 +1110,7 @@
+ | AArch64_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");
+
Home |
Main Index |
Thread Index |
Old Index