pkgsrc-WIP-changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
фвфadasat,gnatcoll-core,gprlib,spark2014,xmlada: remove packages moved to main tree
Module Name: pkgsrc-wip
Committed By: Dmytro Kazankov <dkazankov%NetBSD.org@localhost>
Pushed By: dkazankov
Date: Thu Jul 10 17:39:28 2025 +0300
Changeset: 3ab61e9fff27b49bf08b951fb13558dac88fdc49
Modified Files:
Makefile
Removed Files:
adasat/COMMIT_MSG
adasat/DESCR
adasat/Makefile
adasat/buildlink3.mk
adasat/distinfo
adasat/patches/patch-Makefile
gnatcoll-core/DESCR
gnatcoll-core/Makefile
gnatcoll-core/buildlink3.mk
gnatcoll-core/distinfo
gnatcoll-core/patches/patch-Makefile
gnatcoll-core/patches/patch-core_src_executable__path.c
gnatcoll-core/patches/patch-core_src_os_unix_libc-wrappers.c
gnatcoll-core/patches/patch-core_src_os_unix_process-wrappers.c
gnatcoll-core/patches/patch-gprproject_____init____.py
gnatcoll-core/patches/patch-gprproject_gprbuild.py
gprlib/DESCR
gprlib/Makefile
gprlib/buildlink3.mk
gprlib/distinfo
gprlib/patches/patch-Makefile
gprlib/patches/patch-gpr_gpr.gpr
gprlib/patches/patch-gpr_src_gpr-util-put__resource__usage____unix.adb
gprlib/patches/patch-gpr_src_gpr-version.ads
gprlib/patches/patch-gpr_src_gpr_imports.c
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_semaphores__c.c
spark2014/patches/patch-src_common_x86__64-netbsd_platform.adb
spark2014/patches/patch-src_gnatprove_spark__report.adb
spark2014/patches/patch-why3_Makefile.in
xmlada/DESCR
xmlada/Makefile
xmlada/buildlink3.mk
xmlada/distinfo
xmlada/patches/patch-configure
Log Message:
фвфadasat,gnatcoll-core,gprlib,spark2014,xmlada: remove packages moved to main tree
To see a diff of this commit:
https://wip.pkgsrc.org/cgi-bin/gitweb.cgi?p=pkgsrc-wip.git;a=commitdiff;h=3ab61e9fff27b49bf08b951fb13558dac88fdc49
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
diffstat:
Makefile | 5 -
adasat/COMMIT_MSG | 3 -
adasat/DESCR | 7 -
adasat/Makefile | 44 --
adasat/buildlink3.mk | 21 -
adasat/distinfo | 6 -
adasat/patches/patch-Makefile | 42 --
gnatcoll-core/DESCR | 8 -
gnatcoll-core/Makefile | 61 ---
gnatcoll-core/buildlink3.mk | 21 -
gnatcoll-core/distinfo | 11 -
gnatcoll-core/patches/patch-Makefile | 56 --
.../patches/patch-core_src_executable__path.c | 15 -
.../patches/patch-core_src_os_unix_libc-wrappers.c | 30 -
.../patch-core_src_os_unix_process-wrappers.c | 17 -
.../patches/patch-gprproject_____init____.py | 38 --
gnatcoll-core/patches/patch-gprproject_gprbuild.py | 37 --
gprlib/DESCR | 4 -
gprlib/Makefile | 64 ---
gprlib/buildlink3.mk | 21 -
gprlib/distinfo | 10 -
gprlib/patches/patch-Makefile | 77 ---
gprlib/patches/patch-gpr_gpr.gpr | 15 -
...r_src_gpr-util-put__resource__usage____unix.adb | 15 -
gprlib/patches/patch-gpr_src_gpr-version.ads | 28 -
gprlib/patches/patch-gpr_src_gpr_imports.c | 22 -
spark2014/DESCR | 8 -
spark2014/Makefile | 97 ----
spark2014/PLIST | 610 ---------------------
spark2014/buildlink3.mk | 14 -
spark2014/distinfo | 28 -
spark2014/patches/patch-Makefile | 66 ---
spark2014/patches/patch-gnatprove.gpr | 17 -
spark2014/patches/patch-spark2014vsn.ads | 15 -
spark2014/patches/patch-src_common_platform.ads | 15 -
spark2014/patches/patch-src_common_semaphores__c.c | 73 ---
.../patch-src_common_x86__64-netbsd_platform.adb | 44 --
.../patches/patch-src_gnatprove_spark__report.adb | 14 -
spark2014/patches/patch-why3_Makefile.in | 15 -
xmlada/DESCR | 4 -
xmlada/Makefile | 46 --
xmlada/buildlink3.mk | 21 -
xmlada/distinfo | 6 -
xmlada/patches/patch-configure | 15 -
44 files changed, 1786 deletions(-)
diffs:
diff --git a/Makefile b/Makefile
index f0e720676b..fac52e9bab 100644
--- a/Makefile
+++ b/Makefile
@@ -128,7 +128,6 @@ SUBDIR+= ad2vcf
SUBDIR+= ada_gnat
SUBDIR+= ada_xmlada
SUBDIR+= adamem
-SUBDIR+= adasat
SUBDIR+= adept
SUBDIR+= adguardhome
SUBDIR+= adjustmtu
@@ -1310,7 +1309,6 @@ SUBDIR+= gmrun
SUBDIR+= gn-git
SUBDIR+= gnat-glade
SUBDIR+= gnatcoll-bindings
-SUBDIR+= gnatcoll-core
SUBDIR+= gnatcoll-db
SUBDIR+= gnocchi
SUBDIR+= gnochm
@@ -1402,7 +1400,6 @@ SUBDIR+= gp-toric
SUBDIR+= gpak
SUBDIR+= gpatch
SUBDIR+= gplbasic
-SUBDIR+= gprlib
SUBDIR+= gpsdrive
SUBDIR+= gptfdisk
SUBDIR+= gpx2shp
@@ -5424,7 +5421,6 @@ SUBDIR+= spacefm
SUBDIR+= spai
SUBDIR+= spamassassin-cvs
SUBDIR+= spamd-devel
-SUBDIR+= spark2014
SUBDIR+= spatt
SUBDIR+= spcm
SUBDIR+= spectra
@@ -6054,7 +6050,6 @@ SUBDIR+= xmim
SUBDIR+= xml-light
SUBDIR+= xml2tsv
SUBDIR+= xml2tsv-git
-SUBDIR+= xmlada
SUBDIR+= xmlformat-docs
SUBDIR+= xmlformat-perl
SUBDIR+= xmlformat-ruby
diff --git a/adasat/COMMIT_MSG b/adasat/COMMIT_MSG
deleted file mode 100644
index 919cac818a..0000000000
--- a/adasat/COMMIT_MSG
+++ /dev/null
@@ -1,3 +0,0 @@
-math/adasat: Add new package 25.0.0
-
-Implementation of a DPLL-based SAT solver in Ada
diff --git a/adasat/DESCR b/adasat/DESCR
deleted file mode 100644
index b39e61419b..0000000000
--- a/adasat/DESCR
+++ /dev/null
@@ -1,7 +0,0 @@
-Implementation of a DPLL-based SAT solver in Ada
-
-Main features:
-- Conflict analysis and backjumping
-- Two-watched literals scheme
-- Built-in support for At-Most-One constraints
-- Custom theories
diff --git a/adasat/Makefile b/adasat/Makefile
deleted file mode 100644
index c73ba4e63b..0000000000
--- a/adasat/Makefile
+++ /dev/null
@@ -1,44 +0,0 @@
-# $NetBSD: Makefile,v 1.0 2024/05/06 15:00:00 dkazankov Exp $
-
-DISTNAME= AdaSAT-${PKGVERSION_NOREV}
-PKGNAME= adasat-25.0.0
-CATEGORIES= math devel
-MASTER_SITES= ${MASTER_SITE_GITHUB:=AdaCore/}
-GITHUB_PROJECT= AdaSAT
-GITHUB_TAG= v${PKGVERSION_NOREV}
-
-MAINTAINER= dkazankov%NetBSD.org@localhost
-HOMEPAGE= https://github.com/AdaCore/AdaSAT
-COMMENT= Implementation of a DPLL-based SAT solver in Ada
-LICENSE= apache-2.0
-
-USE_TOOLS+= gmake
-
-USE_LANGUAGES= ada
-GCC_REQD+= 13
-
-USE_GCC_RUNTIME= yes
-
-.include "../../mk/bsd.prefs.mk"
-
-USE_PKGSRC_GCC_RUNTIME?= no
-.if ${USE_PKGSRC_GCC_RUNTIME:tl} == "yes"
-ALL_LIBRARY_TYPES= static static-pic relocatable
-.else
-ALL_LIBRARY_TYPES= static
-.endif
-
-MAKE_FLAGS+= BUILD_MODE=prod
-MAKE_FLAGS+= ALL_LIBRARY_TYPES=${ALL_LIBRARY_TYPES:Q}
-BUILD_TARGET= all-libs
-
-INSTALL_MAKE_FLAGS+= INSTALL_DIR=${DESTDIR}${PREFIX}
-INSTALL_MAKE_FLAGS+= ALL_LIBRARY_TYPES=${ALL_LIBRARY_TYPES:Q}
-
-GENERATE_PLIST+= \
- cd ${DESTDIR}${PREFIX} && \
- ${FIND} include lib share \( -type f -or -type l \) -print | ${SORT};
-
-.include "../../devel/gprbuild/buildlink3.mk"
-
-.include "../../mk/bsd.pkg.mk"
diff --git a/adasat/buildlink3.mk b/adasat/buildlink3.mk
deleted file mode 100644
index c7f953a0ea..0000000000
--- a/adasat/buildlink3.mk
+++ /dev/null
@@ -1,21 +0,0 @@
-# $NetBSD: buildlink3.mk,v 1.0 2024/05/14 09:30:00 dkazankov Exp $
-
-BUILDLINK_TREE+= adasat
-
-.if !defined(ADASAT_BUILDLINK3_MK)
-ADASAT_BUILDLINK3_MK:=
-
-BUILDLINK_API_DEPENDS.adasat+= adasat>=24.0.0
-BUILDLINK_ABI_DEPENDS.adasat+= adasat>=25.0.0
-BUILDLINK_PKGSRCDIR.adasat?= ../../wip/adasat
-BUILDLINK_DEPMETHOD.adasat?= build
-
-BUILDLINK_CONTENTS_FILTER.adasat= \
- ${EGREP} '(include/.*\.ad.$$|lib/.*\.ali$$|lib/.*\.a$$|lib/.*\.so.*$$|share/gpr/manifests/.*|share/gpr/.*\.gpr$$)'
-
-pkgbase := adasat
-.include "../../mk/pkg-build-options.mk"
-
-.endif
-
-BUILDLINK_TREE+= -adasat
diff --git a/adasat/distinfo b/adasat/distinfo
deleted file mode 100644
index 0d9b43bb43..0000000000
--- a/adasat/distinfo
+++ /dev/null
@@ -1,6 +0,0 @@
-$NetBSD$
-
-BLAKE2s (AdaSAT-25.0.0.tar.gz) = 82395941685f2006742a211de0129b62097c90c87a47a93da9adbf1ca951f55a
-SHA512 (AdaSAT-25.0.0.tar.gz) = 7781a683c5aef9efa9a6b57e82070184c02d734fcf448aa5aa79d9aaa3b40d181d87d7487d9c204f7dcd584a3d2dc1c9ebc027e82b2532c3418c25a2395fd9af
-Size (AdaSAT-25.0.0.tar.gz) = 30707 bytes
-SHA1 (patch-Makefile) = e75fc73d66601d816efe81ceb8c011fbe2460e0b
diff --git a/adasat/patches/patch-Makefile b/adasat/patches/patch-Makefile
deleted file mode 100644
index 58b6649c3a..0000000000
--- a/adasat/patches/patch-Makefile
+++ /dev/null
@@ -1,42 +0,0 @@
-$NetBSD: patch-Makefile,v 1.0 2024/08/12 23:00:00 dkazankov Exp $
-
-Add gprbuild and gprinstall options
-Make ALL_LIBRARY_TYPES externally settable
-
---- Makefile.orig 2024-01-03 19:00:52.000000000 +0200
-+++ Makefile
-@@ -4,19 +4,23 @@
- BUILD_DIR ?= .
- INSTALL_DIR ?= .
-
--ALL_LIBRARY_TYPES = static static-pic relocatable
-+GPRBUILD_OPTIONS ?= -p -j$(PROCESSORS)
-+GPRINSTALL_OPTIONS =
-+
-+ALL_LIBRARY_TYPES ?= static static-pic relocatable
-
- .PHONY: lib
- lib:
- gprbuild -k -P adasat.gpr -p -j$(PROCESSORS) \
- --relocate-build-tree="$(BUILD_DIR)" \
- -XLIBRARY_TYPE=$(LIBRARY_TYPE) \
-- -XBUILD_MODE=$(BUILD_MODE)
-+ -XBUILD_MODE=$(BUILD_MODE) \
-+ $(GPRBUILD_OPTIONS)
-
- .PHONY: all-libs
- all-libs:
- for kind in $(ALL_LIBRARY_TYPES) ; do \
-- gprbuild -k -P adasat.gpr -p -j$(PROCESSORS) \
-+ gprbuild -k -P adasat.gpr $(GPRBUILD_OPTIONS) \
- --relocate-build-tree="$(BUILD_DIR)" \
- -XLIBRARY_TYPE=$$kind \
- -XBUILD_MODE=$(BUILD_MODE) ; \
-@@ -32,6 +36,7 @@
- --prefix="$(INSTALL_DIR)" \
- --build-name=$$kind \
- --build-var=LIBRARY_TYPE ; \
-+ $(GPRINSTALL_OPTIONS) \
- done
-
- .PHONY: test
diff --git a/gnatcoll-core/DESCR b/gnatcoll-core/DESCR
deleted file mode 100644
index 0c7fb2a568..0000000000
--- a/gnatcoll-core/DESCR
+++ /dev/null
@@ -1,8 +0,0 @@
-The GNAT Components Collection (GNATcoll) - Core packages
-
-The reusable library known as the GNAT Component Collection (GNATColl) is
-based on one main principle: general-purpose packages that are part of
-the GNAT technology should also be available to GNAT user application code.
-The GNATColl components complement the predefined Ada and GNAT libraries
-and deal with a range of common programming issues including string and text
-processing, memory management, and file handling.
diff --git a/gnatcoll-core/Makefile b/gnatcoll-core/Makefile
deleted file mode 100644
index 32870ac21b..0000000000
--- a/gnatcoll-core/Makefile
+++ /dev/null
@@ -1,61 +0,0 @@
-# $NetBSD: Makefile,v 1.0 2024/05/06 15:00:00 dkazankov Exp $
-
-DISTNAME= gnatcoll-core-${PKGVERSION_NOREV}
-PKGNAME= gnatcoll-core-25.0.0
-CATEGORIES= devel
-MASTER_SITES= ${MASTER_SITE_GITHUB:=AdaCore/}
-GITHUB_PROJECT= gnatcoll-core
-GITHUB_TAG= v${PKGVERSION_NOREV}
-
-MAINTAINER= dkazankov%NetBSD.org@localhost
-HOMEPAGE= https://github.com/AdaCore/gnatcoll-core
-COMMENT= The GNAT Components Collection (GNATcoll) - Core packages
-LICENSE= gnu-gpl-v3
-
-USE_TOOLS+= gmake grep
-
-USE_LANGUAGES= c ada
-
-GCC_REQD+= 13
-
-USE_GCC_RUNTIME= yes
-
-.include "../../mk/bsd.prefs.mk"
-
-# Use C preprocessed symbols on NetBSD
-.if ${OPSYS} == "NetBSD"
-SUBST_CLASSES+= ldl
-SUBST_MESSAGE.ldl= Fix extra libs on NetBSD in ${SUBST_FILES.ldl}
-SUBST_STAGE.ldl= pre-configure
-SUBST_FILES.ldl= core/gnatcoll_core.gpr
-SUBST_SED.ldl= -e "s,\"-ldl\",\"\","
-
-SUBST_CLASSES+= opendir
-SUBST_MESSAGE.opendir= Replace opendir with __gnatcoll_opendir in ${SUBST_FILES.opendir}
-SUBST_STAGE.opendir= pre-configure
-SUBST_FILES.opendir= core/src/os/unix/gnatcoll-os-libc-dirent.ads
-SUBST_SED.opendir= -e "s,\"opendir\",\"__gnatcoll_opendir\","
-.endif
-
-MAKE_FLAGS+= prefix=${DESTDIR}${PREFIX} BUILD=PROD
-
-USE_PKGSRC_GCC_RUNTIME?= no
-.if ${USE_PKGSRC_GCC_RUNTIME:tl} == "yes"
-MAKE_FLAGS+= ENABLE_SHARED=yes
-BUILDLINK_DEPMETHOD.xmlada= full
-BUILDLINK_DEPMETHOD.gprlib= full
-.else
-MAKE_FLAGS+= ENABLE_SHARED=no
-.endif
-
-GENERATE_PLIST+= \
- cd ${DESTDIR}${PREFIX} && \
- ${FIND} include lib share \( -type f -or -type l \) -print | ${SORT};
-
-.include "../../devel/gprbuild/buildlink3.mk"
-.include "../../wip/xmlada/buildlink3.mk"
-.include "../../wip/gprlib/buildlink3.mk"
-
-.include "../../lang/python/tool.mk"
-
-.include "../../mk/bsd.pkg.mk"
diff --git a/gnatcoll-core/buildlink3.mk b/gnatcoll-core/buildlink3.mk
deleted file mode 100644
index c9a6b71e64..0000000000
--- a/gnatcoll-core/buildlink3.mk
+++ /dev/null
@@ -1,21 +0,0 @@
-# $NetBSD: buildlink3.mk,v 1.0 2024/05/06 13:00:00 dkazankov Exp $
-
-BUILDLINK_TREE+= gnatcoll-core
-
-.if !defined(GNATCOLL_CORE_BUILDLINK3_MK)
-GNATCOLL_CORE_BUILDLINK3_MK:=
-
-BUILDLINK_API_DEPENDS.gnatcoll-core+= gnatcoll-core>=24.0.0
-BUILDLINK_ABI_DEPENDS.gnatcoll-core+= gnatcoll-core>=25.0.0
-BUILDLINK_PKGSRCDIR.gnatcoll-core?= ../../wip/gnatcoll-core
-BUILDLINK_DEPMETHOD.gnatcoll-core?= build
-
-BUILDLINK_CONTENTS_FILTER.gnatcoll-core= \
- ${EGREP} '(include/.*\.ad.$$|lib/.*\.ali$$|lib/.*\.a$$|lib/libgnatcoll.*$$|share/gpr/manifests/gnatcoll.*|share/gpr/gnatcoll.*\.gpr$$)'
-
-pkgbase := gnatcoll-core
-.include "../../mk/pkg-build-options.mk"
-
-.endif
-
-BUILDLINK_TREE+= -gnatcoll-core
diff --git a/gnatcoll-core/distinfo b/gnatcoll-core/distinfo
deleted file mode 100644
index e33bb9fc48..0000000000
--- a/gnatcoll-core/distinfo
+++ /dev/null
@@ -1,11 +0,0 @@
-$NetBSD$
-
-BLAKE2s (gnatcoll-core-25.0.0.tar.gz) = 4e3053b10a27ea4bd4fc1c8ba2e8ab936087507f8969e9c71b33c0fbb5a81a4c
-SHA512 (gnatcoll-core-25.0.0.tar.gz) = efa19b9760bd16b402445d4932dfd28f087f9a09b91ec688c6976b7b83fe5986580b1871378ac024e9a712df8ee75963e5dc88629a72ee1ce76f1d1403b8e122
-Size (gnatcoll-core-25.0.0.tar.gz) = 7492612 bytes
-SHA1 (patch-Makefile) = 5a6a41fadcd84fa0eda5122263fbb3dee601b546
-SHA1 (patch-core_src_executable__path.c) = a4105333ea497cae722b2870149725f69de2dbe9
-SHA1 (patch-core_src_os_unix_libc-wrappers.c) = 322ecd62a2b35febec07f1195b4cfd2f098a2556
-SHA1 (patch-core_src_os_unix_process-wrappers.c) = ef3696e8098b9ca434a83093aa53698c578fd0cc
-SHA1 (patch-gprproject_____init____.py) = ac5ac38f93b4b6e11627aecc2cca84e3d3d6c4e6
-SHA1 (patch-gprproject_gprbuild.py) = 96bbf5565e72465da06e53c1eb38c81f1e3c3af7
diff --git a/gnatcoll-core/patches/patch-Makefile b/gnatcoll-core/patches/patch-Makefile
deleted file mode 100644
index 87b10089da..0000000000
--- a/gnatcoll-core/patches/patch-Makefile
+++ /dev/null
@@ -1,56 +0,0 @@
-$NetBSD: patch-Makefile,v 1.0 2024/11/27 11:00:00 dkazankov Exp $
-
-Fix target calculation
-Add necessary parameters for pkgsrc build
-Fix destdir building in rsync absence
-
---- Makefile.orig 2024-09-24 12:28:32.000000000 +0300
-+++ Makefile
-@@ -61,7 +61,7 @@
- GNATCOLL_GPR=$(SOURCE_DIR)/gnatcoll.gpr
-
- TARGET := $(shell gcc -dumpmachine)
--NORMALIZED_TARGET := $(subst normalized_target:,,$(wordlist 6,6,$(shell gprconfig --config=ada --target=$(TARGET) --mi-show-compilers)))
-+NORMALIZED_TARGET := $(lastword $(subst :, ,$(shell gprconfig --config=ada --target=$(TARGET) --mi-show-compilers | grep ' 1 normalized_target:')))
- ifeq ($(NORMALIZED_TARGET),)
- $(error No toolchain found for target "$(TARGET)")
- endif
-@@ -98,8 +98,13 @@
- --build=$(BUILD) \
- --target=$(NORMALIZED_TARGET) \
- --prefix=local-install \
-- --install \
-- --enable-shared=$(ENABLE_SHARED)
-+ --enable-shared=$(ENABLE_SHARED) \
-+ --add-gpr-path='./minimal,./core,./projects' \
-+ --gpr-opts $(GPRBUILD_OPTIONS)
-+
-+INSTALL_ARGS= \
-+ --prefix=local-install \
-+ --gpr-opts $(GPRINSTALL_OPTIONS)
-
- build:
- rm -rf local-install
-@@ -112,18 +117,21 @@
- endif
-
- $(PYTHON) $(SOURCE_DIR)/minimal/gnatcoll_minimal.gpr.py build $(INSTR_BUILD_OPTS) $(BUILD_ARGS)
-+ $(PYTHON) $(SOURCE_DIR)/minimal/gnatcoll_minimal.gpr.py install $(INSTALL_ARGS)
-
- ifeq ($(GNATCOLL_MINIMAL_ONLY), no)
- $(PYTHON) $(SOURCE_DIR)/core/gnatcoll_core.gpr.py build $(INSTR_BUILD_OPTS) $(BUILD_ARGS)
-+ $(PYTHON) $(SOURCE_DIR)/core/gnatcoll_core.gpr.py install $(INSTALL_ARGS)
- endif
-
- ifeq ($(GNATCOLL_PROJECTS), yes)
- $(PYTHON) $(SOURCE_DIR)/projects/gnatcoll_projects.gpr.py build $(INSTR_BUILD_OPTS) $(BUILD_ARGS)
-+ $(PYTHON) $(SOURCE_DIR)/projects/gnatcoll_projects.gpr.py install $(INSTALL_ARGS)
- endif
-
- install:
- @echo "Installing gnatcoll into $(prefix)"
-- rsync -av ./local-install/ $(prefix)$(integrated_install)
-+ cp -r ./local-install/* $(prefix)$(integrated_install)
-
- ###########
- # Cleanup #
diff --git a/gnatcoll-core/patches/patch-core_src_executable__path.c b/gnatcoll-core/patches/patch-core_src_executable__path.c
deleted file mode 100644
index 65cc519b88..0000000000
--- a/gnatcoll-core/patches/patch-core_src_executable__path.c
+++ /dev/null
@@ -1,15 +0,0 @@
-$NetBSD: patch-executable_path.c,v 1.0 2024/05/06 14:00:00 dkazankov Exp $
-
-Add NetBSD support
-
---- core/src/executable_path.c.orig 2024-09-24 12:28:32.000000000 +0300
-+++ core/src/executable_path.c
-@@ -50,7 +50,7 @@
- return (int) GetModuleFileNameA(NULL, buffer, (DWORD) size);
- }
-
--#elif defined (__linux__)
-+#elif defined (__linux__) || defined (__NetBSD__)
- /* Linux implementation */
- #include <unistd.h>
- int
diff --git a/gnatcoll-core/patches/patch-core_src_os_unix_libc-wrappers.c b/gnatcoll-core/patches/patch-core_src_os_unix_libc-wrappers.c
deleted file mode 100644
index 43a8dfb37f..0000000000
--- a/gnatcoll-core/patches/patch-core_src_os_unix_libc-wrappers.c
+++ /dev/null
@@ -1,30 +0,0 @@
-$NetBSD: patch-src_os_unix_libc-wrappers.c,v 1.0 2024/05/10 23:00:00 dkazankov Exp $
-
-Fix linker version warning on NetBSD
-Add NetBSD support
-
---- core/src/os/unix/libc-wrappers.c.orig 2024-09-24 12:28:32.000000000 +0300
-+++ core/src/os/unix/libc-wrappers.c
-@@ -400,6 +400,13 @@
- char name[GNATCOLL_DIRENT_NAME_MAX];
- };
-
-+#if defined(__NetBSD__)
-+DIR * __gnatcoll_opendir(const char *filename)
-+{
-+ return opendir(filename);
-+}
-+#endif
-+
- void __gnatcoll_readdir(DIR *dirp, struct gnatcoll_dirent *buf)
- {
- struct dirent *result;
-@@ -409,7 +416,7 @@
- if (result != NULL)
- {
- buf->inode = (uint_64) result->d_ino;
--#if defined(__APPLE__)
-+#if defined(__APPLE__) || defined(__NetBSD__)
- buf->offset = 0;
- #else
- buf->offset = (uint_64) result->d_off;
diff --git a/gnatcoll-core/patches/patch-core_src_os_unix_process-wrappers.c b/gnatcoll-core/patches/patch-core_src_os_unix_process-wrappers.c
deleted file mode 100644
index 75a2b1d6ff..0000000000
--- a/gnatcoll-core/patches/patch-core_src_os_unix_process-wrappers.c
+++ /dev/null
@@ -1,17 +0,0 @@
-$NetBSD: patch-src_os_unix_process-wrappers.c,v 1.0 2024/05/10 23:00:00 dkazankov Exp $
-
-Add NetBSD support
-
---- core/src/os/unix/process-wrappers.c.orig 2024-09-24 12:28:32.000000000 +0300
-+++ core/src/os/unix/process-wrappers.c
-@@ -28,6 +28,10 @@
- #include <unistd.h>
- #include <sys/wait.h>
- #include <signal.h>
-+#if defined(__NetBSD__)
-+#include <sys/select.h>
-+#include <sys/time.h>
-+#endif
-
- typedef long long int sint_64;
-
diff --git a/gnatcoll-core/patches/patch-gprproject_____init____.py b/gnatcoll-core/patches/patch-gprproject_____init____.py
deleted file mode 100644
index f1d7a9082e..0000000000
--- a/gnatcoll-core/patches/patch-gprproject_____init____.py
+++ /dev/null
@@ -1,38 +0,0 @@
-$NetBSD: patch-gprproject_____init____.py,v 1.0 2024/11/27 11:00:00 dkazankov Exp $
-
-Fix parameters throughput
-
---- gprproject/__init__.py.orig 2024-09-24 12:28:32.000000000 +0300
-+++ gprproject/__init__.py
-@@ -173,7 +173,7 @@
- print(f'{var:<32} := "{value}";')
-
- if not args.configure_only:
-- status = gpr.build([])
-+ status = gpr.build(args.gpr_opts)
- if status == 0 and args.install:
- status = gpr.install([])
- return status
-@@ -182,19 +182,19 @@
-
- def clean(self, args):
- gpr = GPRTool.load(self.project_file)
-- return gpr.clean([])
-+ return gpr.clean(args.gpr_opts)
-
- def install(self, args):
- gpr = GPRTool.load(self.project_file)
- if args.prefix:
- gpr.prefix = os.path.abspath(args.prefix)
-- return gpr.install([])
-+ return gpr.install(args.gpr_opts)
-
- def uninstall(self, args):
- gpr = GPRTool.load(self.project_file)
- if args.prefix:
- gpr.prefix = os.path.abspath(args.prefix)
-- return gpr.uninstall([])
-+ return gpr.uninstall(args.gpr_opts)
-
- def add_arguments(self, parser: argparse.ArgumentParser) -> None:
- """Function to be used by end user to add switch to the build command.
diff --git a/gnatcoll-core/patches/patch-gprproject_gprbuild.py b/gnatcoll-core/patches/patch-gprproject_gprbuild.py
deleted file mode 100644
index 96249671e8..0000000000
--- a/gnatcoll-core/patches/patch-gprproject_gprbuild.py
+++ /dev/null
@@ -1,37 +0,0 @@
-$NetBSD: patch-gprproject_gprbuild.py,v 1.0 2025/02/10 13:00:00 dkazankov Exp $
-
-Fix duplicate gprconfig call
-
---- gprproject/gprbuild.py.orig 2024-09-24 12:28:32.000000000 +0300
-+++ gprproject/gprbuild.py
-@@ -59,8 +59,14 @@
- gprconfig_cmd = [which("gprconfig"), "--config=ada", "--mi-show-compilers"]
- if self.original_target:
- gprconfig_cmd.append(f"--target={self.original_target}")
-- gprconfig_output = self.capture(gprconfig_cmd)
-- self.target = re.findall(r" 1 normalized_target:(\S*)", gprconfig_output)[0]
-+
-+ if not target or not prefix:
-+ gprconfig_output = self.capture(gprconfig_cmd)
-+
-+ if target:
-+ self.target = target
-+ else:
-+ self.target = re.findall(r" 1 normalized_target:(\S*)", gprconfig_output)[0]
-
- # Compute default prefix
- if prefix:
-@@ -84,9 +90,10 @@
-
- self.gnatcov = gnatcov
- self.symcc = symcc
-- self.gpr_paths: list[str] = []
-- if self.gpr_paths:
-- self.gpr_paths = list(gpr_paths)
-+ self.gpr_paths = gpr_paths
-+ if gpr_paths:
-+ if type(gpr_paths) is str:
-+ self.gpr_paths: list[str] = gpr_paths.split(",")
- else:
- self.gpr_paths = []
-
diff --git a/gprlib/DESCR b/gprlib/DESCR
deleted file mode 100644
index 2158837c4b..0000000000
--- a/gprlib/DESCR
+++ /dev/null
@@ -1,4 +0,0 @@
-LIBGPR development libraries
-
-GPRbuild is an advanced build system designed to help automate the construction
-of multi-language systems
diff --git a/gprlib/Makefile b/gprlib/Makefile
deleted file mode 100644
index f487436ab9..0000000000
--- a/gprlib/Makefile
+++ /dev/null
@@ -1,64 +0,0 @@
-# $NetBSD: Makefile,v 1.0 2024/05/06 15:00:00 dkazankov Exp $
-
-DISTNAME= gprbuild-${PKGVERSION_NOREV}
-PKGNAME= gprlib-25.0.0
-CATEGORIES= devel
-MASTER_SITES= ${MASTER_SITE_GITHUB:=AdaCore/}
-GITHUB_PROJECT= gprbuild
-GITHUB_TAG= v${PKGVERSION_NOREV}
-
-MAINTAINER= dkazankov%NetBSD.org@localhost
-HOMEPAGE= https://github.com/AdaCore/gprbuild
-COMMENT= LIBGPR development libraries
-LICENSE= gnu-gpl-v3
-
-USE_TOOLS+= gmake
-HAS_CONFIGURE= yes
-
-USE_LANGUAGES= c ada
-
-GCC_REQD+= 13
-
-# GPRLIB 25 uses -gnat2020 switch
-USE_ADA_FEATURES= gnat2020
-
-USE_GCC_RUNTIME= yes
-
-.include "../../mk/bsd.prefs.mk"
-
-# Use C preprocessed symbols on NetBSD
-.if ${OPSYS} == "NetBSD"
-SUBST_CLASSES+= getrusage
-SUBST_MESSAGE.getrusage= Replace getrusage with __netbsd_getrusage in ${SUBST_FILES.getrusage}
-SUBST_STAGE.getrusage= pre-configure
-SUBST_FILES.getrusage= gpr/src/gpr-util-put_resource_usage__unix.adb
-SUBST_SED.getrusage= -e "s,\"getrusage\",\"__netbsd_getrusage\","
-.endif
-
-CONFIGURE_ARGS+= prefix=${DESTDIR}${PREFIX}
-
-USE_PKGSRC_GCC_RUNTIME?= no
-.if ${USE_PKGSRC_GCC_RUNTIME:tl} == "yes"
-CONFIGURE_ARGS+= ENABLE_SHARED=yes
-BUILDLINK_DEPMETHOD.xmlada= full
-.else
-CONFIGURE_ARGS+= ENABLE_SHARED=no
-.endif
-
-do-configure:
- ${RUN}${_ULIMIT_CMD} \
- cd ${WRKSRC} && \
- ${PKGSRC_SETENV} ${CONFIGURE_ENV} \
- ${MAKE_PROGRAM} ${CONFIGURE_ARGS} setup
-
-BUILD_TARGET= libgpr.build
-INSTALL_TARGET= libgpr.install
-
-GENERATE_PLIST+= \
- cd ${DESTDIR}${PREFIX} && \
- ${FIND} include lib share \( -type f -or -type l \) -print | ${SORT};
-
-.include "../../devel/gprbuild/buildlink3.mk"
-.include "../../wip/xmlada/buildlink3.mk"
-
-.include "../../mk/bsd.pkg.mk"
diff --git a/gprlib/buildlink3.mk b/gprlib/buildlink3.mk
deleted file mode 100644
index d4ad251b7d..0000000000
--- a/gprlib/buildlink3.mk
+++ /dev/null
@@ -1,21 +0,0 @@
-# $NetBSD: buildlink3.mk,v 1.0 2024/05/06 18:00:00 dkazankov Exp $
-
-BUILDLINK_TREE+= gprlib
-
-.if !defined(GPRLIB_BUILDLINK3_MK)
-GPRLIB_BUILDLINK3_MK:=
-
-BUILDLINK_API_DEPENDS.gprlib+= gprlib>=24.0.0
-BUILDLINK_ABI_DEPENDS.gprlib+= gprlib>=25.0.0
-BUILDLINK_PKGSRCDIR.gprlib?= ../../wip/gprlib
-BUILDLINK_DEPMETHOD.gprlib?= build
-
-BUILDLINK_CONTENTS_FILTER.gprlib= \
- ${EGREP} '(include/.*\.ad.$$|lib/.*\.ali$$|lib/.*\.a$$|lib/libgnatprj.*\.so.*$$|share/gpr/manifests/.*|share/gpr/.*\.gpr$$|/gpr\.adb$$|/gpr-util-put_resource_usage__unix\.adb$$)'
-
-pkgbase := gprlib
-.include "../../mk/pkg-build-options.mk"
-
-.endif
-
-BUILDLINK_TREE+= -gprlib
diff --git a/gprlib/distinfo b/gprlib/distinfo
deleted file mode 100644
index eeac7d4602..0000000000
--- a/gprlib/distinfo
+++ /dev/null
@@ -1,10 +0,0 @@
-$NetBSD: distinfo,v 1.2 2024/03/19 13:20:35 wiz Exp $
-
-BLAKE2s (gprbuild-25.0.0.tar.gz) = e9462a136fe46fd9e62e7ba602f746275a41347098f273e90b41cd89c46ce386
-SHA512 (gprbuild-25.0.0.tar.gz) = eb2d7072194323cae90acd0c8683eeb6a806ef6ff2ed4d3496e8b94c5b63dae8a428ec428a3610b380df7e122d7a00d9e9634ef06b5369b165536c99209602ce
-Size (gprbuild-25.0.0.tar.gz) = 940774 bytes
-SHA1 (patch-Makefile) = 56c90f388d955d0a6cb46e8b4f4eb23b73557b0e
-SHA1 (patch-gpr_gpr.gpr) = b18713da0795ebefd241414e5e9171ecfa9b79db
-SHA1 (patch-gpr_src_gpr-util-put__resource__usage____unix.adb) = 73cf60af1123151a4177250ac496384cb55e72ec
-SHA1 (patch-gpr_src_gpr-version.ads) = 04f4ec9ff11efc1142960891613bbc80d55fa669
-SHA1 (patch-gpr_src_gpr_imports.c) = 1b72dd42355c7f7189d4a4a8a7bcf7153f206731
diff --git a/gprlib/patches/patch-Makefile b/gprlib/patches/patch-Makefile
deleted file mode 100644
index d31b849824..0000000000
--- a/gprlib/patches/patch-Makefile
+++ /dev/null
@@ -1,77 +0,0 @@
-$NetBSD: patch-Makefile,v 1.3 2025/02/08 14:14:49 wiz Exp $
-
-Make it possible to set install parameters
-Fix install parameters
-Fix ENABLE_SHARED position
-
---- Makefile.orig 2024-10-07 15:45:16.000000000 +0300
-+++ Makefile
-@@ -34,9 +34,6 @@
- SOURCE_DIR := $(shell dirname "$(MAKEFILE_LIST)")
- LIB_DIR = lib/
-
--# Load current setup if any
---include makefile.setup
--
- # target options for cross-build
- ifeq ($(HOST),$(TARGET))
- GTARGET=
-@@ -45,6 +42,13 @@
- GTARGET=--target=$(TARGET)
- endif
-
-+ENABLE_SHARED := $(shell gprbuild $(GTARGET) -c -q -p \
-+ -P$(MAKEPREFIX)config/test_shared 2>/dev/null && echo "yes")
-+
-+# Load current setup if any
-+-include makefile.setup
-+
-+GPRINSTALL_OPTIONS=
- INSTALLER=$(LIB_INSTALLER)
- EXEC_INSTALLER=$(INSTALLER) -XBUILD=${BUILD}
-
-@@ -61,9 +65,6 @@
- MAKEPREFIX=$(SOURCE_DIR)/
- endif
-
--ENABLE_SHARED := $(shell gprbuild $(GTARGET) -c -q -p \
-- -P$(MAKEPREFIX)config/test_shared 2>/dev/null && echo "yes")
--
- ifeq ($(ENABLE_SHARED), yes)
- LIBGPR_TYPES=static shared static-pic
- else
-@@ -72,21 +73,21 @@
-
- # Make sure Windows's "OS" environment variable does not cause
- # confusion for cross-Linux builds.
--LIBGPR_OS = $(if $(findstring linux,$(TARGET)),-XOS=UNIX)
-+LIBGPR_OS = $(if $(or $(findstring linux,$(TARGET)),$(findstring bsd,$(TARGET))),-XOS=UNIX)
-
- # Used to pass extra options to GPRBUILD, like -d for instance
- GPRBUILD_OPTIONS=
-
- BUILDER=gprbuild -p -m $(GTARGET) $(RBD) -j${PROCESSORS} -XBUILD=${BUILD} ${GPRBUILD_OPTIONS}
--LIB_INSTALLER=gprinstall -p -f --target=$(TARGET) $(RBD) "--prefix=${prefix}"
-+LIB_INSTALLER=gprinstall -p -f $(GTARGET) $(RBD) "--prefix=${prefix}" ${GPRINSTALL_OPTIONS}
- CLEANER=gprclean -q $(RBD)
-
- GPRBUILD_BUILDER=$(BUILDER) $(GPRBUILD_GPR) \
-- -XLIBRARY_TYPE=static -XXMLADA_BUILD=static
-+ -XLIBRARY_TYPE=static-pic -XXMLADA_BUILD=static-pic
- LIBGPR_BUILDER=$(BUILDER) $(GPR_GPR) $(LIBGPR_OS)
- LIBGPR_INSTALLER=$(LIB_INSTALLER) $(GPR_GPR) $(LIBGPR_OS) -XBUILD=${BUILD} \
- --install-name=gpr \
-- --build-var=LIBRARY_TYPE --build-var=GPR_BUILD $(GTARGET)
-+ --build-var=LIBRARY_TYPE --build-var=GPR_BUILD
- LIBGPR_UNINSTALLER=$(LIB_INSTALLER) $(GPR_GPR) $(LIBGPR_OS) --install-name=gpr --uninstall
-
- #########
-@@ -127,7 +128,7 @@
- install:
- $(EXEC_INSTALLER) --mode=usage --install-name=gprbuild \
- -XINSTALL_MODE=nointernal $(GPRBUILD_GPR)
-- $(EXEC_INSTALLER) --target=$(TARGET) --mode=usage --install-name=gprbuild \
-+ $(EXEC_INSTALLER) --mode=usage --install-name=gprbuild \
- -XINSTALL_MODE=internal $(GPRBUILD_GPR)
-
- complete: all install libgpr.install.static
diff --git a/gprlib/patches/patch-gpr_gpr.gpr b/gprlib/patches/patch-gpr_gpr.gpr
deleted file mode 100644
index b05b9e9569..0000000000
--- a/gprlib/patches/patch-gpr_gpr.gpr
+++ /dev/null
@@ -1,15 +0,0 @@
-$NetBSD: patch-gpr_gpr.gpr,v 1.4 2025/02/08 14:14:49 wiz Exp $
-
-Fix name conflict with grpc - same as linux distros
-
---- gpr/gpr.gpr.orig 2023-10-09 21:31:11.000000000 +0300
-+++ gpr/gpr.gpr
-@@ -38,7 +38,7 @@
-
- for Source_Dirs use ("src");
-
-- for Library_Name use "gpr";
-+ for Library_Name use "gnatprj";
- for Object_Dir use "libobj/" & Bld & "/" & Gnat_Lib_Type;
- for Library_Dir use "lib/" & Bld & "/" & Gnat_Lib_Type;
-
diff --git a/gprlib/patches/patch-gpr_src_gpr-util-put__resource__usage____unix.adb b/gprlib/patches/patch-gpr_src_gpr-util-put__resource__usage____unix.adb
deleted file mode 100644
index 7626f27f2f..0000000000
--- a/gprlib/patches/patch-gpr_src_gpr-util-put__resource__usage____unix.adb
+++ /dev/null
@@ -1,15 +0,0 @@
-$NetBSD: patch-gpr_src_gpr-util-put__resource__usage____unix.adb,v 1.1 2024/05/07 11:00:00 dkazankov Exp $
-
-Fix warning at link stage on NetBSD
-
---- gpr/src/gpr-util-put_resource_usage__unix.adb.orig 2023-10-09 21:31:11.000000000 +0300
-+++ gpr/src/gpr-util-put_resource_usage__unix.adb
-@@ -69,7 +69,7 @@
- procedure Print (This : STC.Timeval);
-
- function Getrusage (Who : Integer; usage : out Rusage) return Integer
-- with Import, Convention => C;
-+ with Import, Convention => C, External_Name => "getrusage";
-
- -----------
- -- Print --
diff --git a/gprlib/patches/patch-gpr_src_gpr-version.ads b/gprlib/patches/patch-gpr_src_gpr-version.ads
deleted file mode 100644
index 0ef0e62008..0000000000
--- a/gprlib/patches/patch-gpr_src_gpr-version.ads
+++ /dev/null
@@ -1,28 +0,0 @@
-$NetBSD: patch-gpr_src_gpr-version.ads,v 1.1 2024/03/19 13:20:35 wiz Exp $
-
-Fix incorrect version reporting
-
---- gpr/src/gpr-version.ads.orig 2023-10-09 21:31:11.000000000 +0300
-+++ gpr/src/gpr-version.ads
-@@ -30,17 +30,17 @@
-
- package GPR.Version is
-
-- Gpr_Version : constant String := "18.0w";
-+ Gpr_Version : constant String := "25.0w";
- -- Static string identifying this version
-
-- Date : constant String := "19940713";
-+ Date : constant String := "20241126";
-
-- Current_Year : constant String := "2016";
-+ Current_Year : constant String := "2024";
-
- type Gnat_Build_Type is (Gnatpro, FSF, GPL);
- -- See Get_Gnat_Build_Type below for the meaning of these values
-
-- Build_Type : constant Gnat_Build_Type := Gnatpro;
-+ Build_Type : constant Gnat_Build_Type := FSF;
- -- Kind of GNAT Build:
- --
- -- FSF
diff --git a/gprlib/patches/patch-gpr_src_gpr_imports.c b/gprlib/patches/patch-gpr_src_gpr_imports.c
deleted file mode 100644
index d82851813a..0000000000
--- a/gprlib/patches/patch-gpr_src_gpr_imports.c
+++ /dev/null
@@ -1,22 +0,0 @@
-$NetBSD: patch-gpr_src_gpr_imports.c,v 1.1 2024/03/12 17:50:13 wiz Exp $
-
-Add support for NetBSD (same as for FreeBSD) and fix getrusage() warning at linking stage
-
---- gpr/src/gpr_imports.c.orig 2023-10-09 21:31:11.000000000 +0300
-+++ gpr/src/gpr_imports.c
-@@ -64,6 +64,15 @@
- char __gnat_shared_libgcc_default = STATIC;
- const char *__gnat_default_libgcc_subdir = "lib";
-
-+#elif defined(__NetBSD__)
-+int __gnat_link_max = 8192;
-+char __gnat_shared_libgcc_default = STATIC;
-+const char *__gnat_default_libgcc_subdir = "lib";
-+#include "sys/resource.h"
-+int __netbsd_getrusage(int who, struct rusage *rusage) {
-+ return getrusage(who, rusage);
-+}
-+
- #elif defined (__APPLE__)
- int __gnat_link_max = 262144;
- char __gnat_shared_libgcc_default = SHARED;
diff --git a/spark2014/DESCR b/spark2014/DESCR
deleted file mode 100644
index 81e09a4aba..0000000000
--- a/spark2014/DESCR
+++ /dev/null
@@ -1,8 +0,0 @@
-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
deleted file mode 100644
index 8016a720a1..0000000000
--- a/spark2014/Makefile
+++ /dev/null
@@ -1,97 +0,0 @@
-# $NetBSD: Makefile,v 1.2 2024/05/31 14:00:00 dkazankov Exp $
-
-DISTNAME= spark2014
-PKGNAME= spark2014-13.3.0
-CATEGORIES= lang devel
-MASTER_SITES= ${MASTER_SITE_GITHUB:=AdaCore/}
-GITHUB_PROJECT= spark2014
-# latest fsf-13 branch commit
-GITHUB_TAG= 12db22e854defa9d1c993ef904af1e72330a68ca
-DISTFILES= ${DEFAULT_DISTFILES}
-
-MAINTAINER= dkazankov%NetBSD.org@localhost
-HOMEPAGE= https://github.com/AdaCore/spark2014
-COMMENT= SPARK 2014 toolset
-LICENSE= gnu-gpl-v3
-
-USE_LANGUAGES= c ada
-USE_TOOLS+= gmake
-# GNAT major release must match SPARK2014 major release
-GCC_REQD+= 13
-
-HAS_CONFIGURE= yes
-
-MKPIE_SUPPORTED= no
-RELRO_SUPPORTED= no
-
-GITHUB_SUBMODULES+= AdaCore alt-ergo be23b7992464438d6b654d9e36e6917748862130 alt-ergo
-GITHUB_SUBMODULES+= AdaCore cvc5 98b5fb70e8a94fd258bfc959c4a6fd0cc3537564 cvc5
-GITHUB_SUBMODULES+= AdaCore why3 52b6a590ba9bfc64aa0d22b41715358f26124a1f why3
-GITHUB_SUBMODULES+= AdaCore z3 7e79f0deb7c9d43f7637113be5b99391f14fcc2e z3
-
-GCC_DIST_VERSION= 13.3.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}/}
-
-.include "../../mk/bsd.prefs.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'
-
-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} bin \( -type f -or -type l \) -print | ${SORT};
-
-.include "../../devel/gprbuild/buildlink3.mk"
-
-.include "../../wip/xmlada/buildlink3.mk"
-.include "../../wip/gprlib/buildlink3.mk"
-.include "../../wip/gnatcoll-core/buildlink3.mk"
-
-.include "../../lang/python/tool.mk"
-
-BUILDLINK_DEPMETHOD.ocaml= build
-.include "../../lang/ocaml/ocaml.mk"
-BUILDLINK_DEPMETHOD.ocamlgraph= build
-.include "../../devel/ocamlgraph/buildlink3.mk"
-BUILDLINK_DEPMETHOD.menhir= build
-.include "../../devel/menhir/buildlink3.mk"
-BUILDLINK_DEPMETHOD.ocaml-zarith= build
-.include "../../math/ocaml-zarith/buildlink3.mk"
-BUILDLINK_DEPMETHOD.ocaml-zip= build
-.include "../../archivers/ocaml-zip/buildlink3.mk"
-BUILDLINK_DEPMETHOD.ocaml-ocplib-simplex= build
-.include "../../math/ocaml-ocplib-simplex/buildlink3.mk"
-BUILDLINK_DEPMETHOD.ocaml-num= build
-.include "../../math/ocaml-num/buildlink3.mk"
-BUILDLINK_DEPMETHOD.ocaml-yojson= build
-.include "../../devel/ocaml-yojson/buildlink3.mk"
-
-.include "../../mk/pthread.buildlink3.mk"
-
-.include "../../mk/bsd.pkg.mk"
diff --git a/spark2014/PLIST b/spark2014/PLIST
deleted file mode 100644
index 8cf0e33229..0000000000
--- a/spark2014/PLIST
+++ /dev/null
@@ -1,610 +0,0 @@
-@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
deleted file mode 100644
index ad07224609..0000000000
--- a/spark2014/buildlink3.mk
+++ /dev/null
@@ -1,14 +0,0 @@
-# $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
-
-.endif
-
-BUILDLINK_TREE+= -spark2014
diff --git a/spark2014/distinfo b/spark2014/distinfo
deleted file mode 100644
index 8e9155f7fd..0000000000
--- a/spark2014/distinfo
+++ /dev/null
@@ -1,28 +0,0 @@
-$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.3.0.tar.xz) = d204b8987b4780b569f28226cbfff34ae27124e529857c36ff90d5d40ef0b511
-SHA512 (gcc-13.3.0.tar.xz) = ed5f2f4c6ed2c796fcf2c93707159e9dbd3ddb1ba063d549804dd68cdabbb6d550985ae1c8465ae9a336cfe29274a6eb0f42e21924360574ebd8e5d5c7c9a801
-Size (gcc-13.3.0.tar.xz) = 87909952 bytes
-BLAKE2s (spark2014-12db22e854defa9d1c993ef904af1e72330a68ca.tar.gz) = 32b2081dfd7bbb4442bc791848cc4900a8cb9214e69fce6b55ef3724b2c9b145
-SHA512 (spark2014-12db22e854defa9d1c993ef904af1e72330a68ca.tar.gz) = 17644c49e642b2e79cfe481414d12df5b27bad003cdabbb0c9e88f5eb1f8b705b159791612a2d5f720e67017f0867ffaa5cfa0bc5fae8188442cd15fb456890b
-Size (spark2014-12db22e854defa9d1c993ef904af1e72330a68ca.tar.gz) = 11924977 bytes
-SHA1 (patch-Makefile) = e27afdf221bd7d527ba2e2d1046d67690319481c
-SHA1 (patch-gnatprove.gpr) = 7ee0cb8d24c8b063431d5ecd8a4e1291a48c5980
-SHA1 (patch-spark2014vsn.ads) = ab6a841bf7398c2f3b8df312463cbbcc59a02808
-SHA1 (patch-src_common_platform.ads) = a81254a67a3a847e1d1de35b310d1b8d9a442c69
-SHA1 (patch-src_common_semaphores__c.c) = 70f91a26919bca7772c35cbf211b38ab5c4cadd3
-SHA1 (patch-src_common_x86__64-netbsd_platform.adb) = eda3cf7f68c989280f9e684e9a5d9188ef41e690
-SHA1 (patch-src_gnatprove_spark__report.adb) = ef2941bb82881ab1f718dfec72764871c672f965
-SHA1 (patch-why3_Makefile.in) = 5d8385d634f1d4385109ec11ce5c239df85b2f51
diff --git a/spark2014/patches/patch-Makefile b/spark2014/patches/patch-Makefile
deleted file mode 100644
index 4ed29a86fe..0000000000
--- a/spark2014/patches/patch-Makefile
+++ /dev/null
@@ -1,66 +0,0 @@
-$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
-@@ -41,7 +41,9 @@
- install-all why3 all setup all-nightly doc-nightly run-benchmark \
- create-benchmark
-
--INSTALLDIR=$(CURDIR)/install
-+PREFIX=
-+DESTDIR=
-+INSTALLDIR=$(DESTDIR)$(PREFIX)
- SHAREDIR=$(INSTALLDIR)/share
- SIDDIR=$(SHAREDIR)/gnat2why-sids
- INCLUDEDIR=$(INSTALLDIR)/include/spark
-@@ -55,9 +57,10 @@
- DOC=ug lrm
- # Control if gnatprove is built in production or debug mode
- PROD=-XBuild=Production
-+GPRARGS='$(PROD)'
- CP=cp -pr
- MV=mv -f
--VERSION=0.0w
-+VERSION='FSF 13.0'
-
- # main target for developers
- all: gnat2why gnatprove why3
-@@ -78,7 +81,7 @@
- # install-all install of gnatprove and why3
-
- setup:
-- cd why3 && ./configure --prefix=$(INSTALLDIR)/libexec/spark \
-+ cd why3 && ./configure --prefix=$(PREFIX)/libexec/spark \
- --enable-relocation --disable-js-of-ocaml \
- --disable-hypothesis-selection --disable-re
-
-@@ -89,15 +92,16 @@
- install-all:
- $(MAKE) install
- $(MAKE) -C why3 install_spark2014_dev
-- sha256sum install/libexec/spark/bin/gnatwhy3 | cut -d' ' -f1 > install/libexec/spark/bin/gnatwhy3.hash
-+ sha256 -n $(INSTALLDIR)/libexec/spark/bin/gnatwhy3 | cut -d' ' -f1 > $(INSTALLDIR)/libexec/spark/bin/gnatwhy3.hash
- # Create the fake prover scripts to help extract benchmarks.
-- $(CP) benchmark_script/fake_* install/libexec/spark/bin
-+ $(CP) benchmark_script/fake_* $(INSTALLDIR)/libexec/spark/bin
-
- install:
- mkdir -p $(INSTALLDIR)/bin $(CONFIGDIR) $(THEORIESDIR) \
- $(RUNTIMESDIR) $(INCLUDEDIR) $(LIBDIR)
- @echo "Generate default target.atp in $(INSTALLDIR)/bin:"
- gcc -c -gnats spark2014vsn.ads -gnatet=$(INSTALLDIR)/bin/target.atp
-+ $(CP) install/bin/* $(INSTALLDIR)/bin
- $(CP) share/spark/help.txt $(GNATPROVEDIR)
- $(CP) share/spark/config/* $(CONFIGDIR)
- $(CP) share/spark/theories/*why $(THEORIESDIR)
-@@ -131,7 +135,7 @@
- # This script should be run *ONLY* in developer build not in prod
- # (gnat2why-nightly)
- python3 scripts/why3keywords.py why3/src/core/keywords.ml src/why/why-keywords.adb
-- $(MAKE) -C gnat2why
-+ $(MAKE) -C gnat2why AUTOMATED=1 GPRARGS=$(GPRARGS)
- # (The timestamp of) src/why/xgen/gnat_ast.ml is updated every time `make` is called in
- # `gnat2why`, causing a recompilation of why3 every time because Why3's makefile is
- # based on timestamps not file content. So we check if anything changed before copying.
diff --git a/spark2014/patches/patch-gnatprove.gpr b/spark2014/patches/patch-gnatprove.gpr
deleted file mode 100644
index 555a0e1a15..0000000000
--- a/spark2014/patches/patch-gnatprove.gpr
+++ /dev/null
@@ -1,17 +0,0 @@
-$NetBSD: patch-gnatprove.gpr,v 1.0 2024/05/19 22:00:00 dkazankov Exp $
-
-Add libpthread link on NetBSD
-
---- gnatprove.gpr.orig 2023-01-05 11:22:11.000000000 +0200
-+++ gnatprove.gpr
-@@ -61,6 +61,10 @@
- case Target is
- when "x86-linux" | "x86_64-linux" =>
- for Default_Switches ("Ada") use ("-pthread");
-+ when "x86_64-netbsd" =>
-+ for Default_Switches ("Ada") use ("-lpthread");
-+ for Default_Switches ("C") use ("-lpthread");
-+ for Linker_Options use ("-lpthread");
- when others =>
- null;
- end case;
diff --git a/spark2014/patches/patch-spark2014vsn.ads b/spark2014/patches/patch-spark2014vsn.ads
deleted file mode 100644
index 533f6a0726..0000000000
--- a/spark2014/patches/patch-spark2014vsn.ads
+++ /dev/null
@@ -1,15 +0,0 @@
-$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
-@@ -22,7 +22,7 @@
-
- package SPARK2014VSN is
-
-- SPARK2014_Static_Version_String : constant String := "0.0w";
-+ SPARK2014_Static_Version_String : constant String := "FSF 13.0";
- -- Static string identifying this version, that can be used as an argument
- -- to e.g. pragma Ident.
- --
diff --git a/spark2014/patches/patch-src_common_platform.ads b/spark2014/patches/patch-src_common_platform.ads
deleted file mode 100644
index 265ce31351..0000000000
--- a/spark2014/patches/patch-src_common_platform.ads
+++ /dev/null
@@ -1,15 +0,0 @@
-$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
-@@ -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_semaphores__c.c b/spark2014/patches/patch-src_common_semaphores__c.c
deleted file mode 100644
index 4c2a15e0c0..0000000000
--- a/spark2014/patches/patch-src_common_semaphores__c.c
+++ /dev/null
@@ -1,73 +0,0 @@
-$NetBSD: patch-src_common_semaphores__c.c,v 1.0 2024/05/31 14:00:00 dkazankov Exp $
-
-Fix runtime error caused semaphore names on NetBSD
-
---- src/common/semaphores_c.c.orig 2023-01-05 11:22:11.000000000 +0200
-+++ src/common/semaphores_c.c
-@@ -30,8 +30,33 @@
- #include <stdio.h>
- #include <stdlib.h>
-
-+#if defined (__NetBSD__)
-+char* __netbsd_sem_name(const char *name) {
-+ size_t len = strlen (name);
-+ char *sem_name = calloc (len+2, sizeof(char));
-+ if (sem_name == NULL) {
-+ return (char *) name;
-+ }
-+ char *p = sem_name;
-+ if (len > 0 && name[0] != '/') {
-+ sem_name[0] = '/';
-+ p++;
-+ }
-+ strcpy (p, name);
-+ return sem_name;
-+}
-+#endif
-+
- sem_t* create_semaphore (const char *name, unsigned int init) {
-+#if defined (__NetBSD__)
-+ char *sem_name = __netbsd_sem_name (name);
-+ sem_t* r = sem_open (sem_name, O_CREAT | O_EXCL, 0600, init);
-+ if (sem_name != name) {
-+ free (sem_name);
-+ }
-+#else
- sem_t* r = sem_open (name, O_CREAT | O_EXCL, 0600, init);
-+#endif
- if (r == SEM_FAILED) {
- perror("failed to create semaphore");
- exit(1);
-@@ -40,7 +65,15 @@
- }
-
- sem_t* open_semaphore (const char *name) {
-+#if defined (__NetBSD__)
-+ char *sem_name = __netbsd_sem_name (name);
-+ sem_t* r = sem_open (sem_name, 0);
-+ if (sem_name != name) {
-+ free (sem_name);
-+ }
-+#else
- sem_t* r = sem_open (name, 0);
-+#endif
- if (r == SEM_FAILED) {
- perror("failed to open semaphore");
- exit(1);
-@@ -70,7 +103,16 @@
- }
-
- void delete_semaphore (const char *name) {
-+#if defined (__NetBSD__)
-+ char *sem_name = __netbsd_sem_name (name);
-+ int r = sem_unlink (sem_name);
-+ if (sem_name != name) {
-+ free (sem_name);
-+ }
-+ if (r == -1) {
-+#else
- if (sem_unlink(name) == -1) {
-+#endif
- // ignore errors of deleting on purpose
- }
- }
diff --git a/spark2014/patches/patch-src_common_x86__64-netbsd_platform.adb b/spark2014/patches/patch-src_common_x86__64-netbsd_platform.adb
deleted file mode 100644
index d3eb781e7e..0000000000
--- a/spark2014/patches/patch-src_common_x86__64-netbsd_platform.adb
+++ /dev/null
@@ -1,44 +0,0 @@
-$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
-+++ src/common/x86_64-netbsd/platform.adb
-@@ -0,0 +1,37 @@
-+------------------------------------------------------------------------------
-+-- --
-+-- GNATPROVE COMPONENTS --
-+-- --
-+-- P L A T F O R M --
-+-- --
-+-- B o d y --
-+-- --
-+-- Copyright (C) 2010-2023, AdaCore --
-+-- --
-+-- gnatprove is free software; you can redistribute it and/or modify it --
-+-- under terms of the GNU General Public License as published by the Free --
-+-- Software Foundation; either version 3, or (at your option) any later --
-+-- version. gnatprove is distributed in the hope that it will be useful, --
-+-- but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHAN- --
-+-- TABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public --
-+-- License for more details. You should have received a copy of the GNU --
-+-- General Public License distributed with gnatprove; see file COPYING3. --
-+-- If not, go to http://www.gnu.org/licenses for a complete copy of the --
-+-- license. --
-+-- --
-+-- gnatprove is maintained by AdaCore (http://www.adacore.com) --
-+-- --
-+------------------------------------------------------------------------------
-+
-+package body Platform is
-+
-+ -------------------
-+ -- Get_OS_Flavor --
-+ -------------------
-+
-+ function Get_OS_Flavor return Host_Operating_System_Flavor is
-+ begin
-+ return X86_64_NetBSD;
-+ end Get_OS_Flavor;
-+
-+end Platform;
diff --git a/spark2014/patches/patch-src_gnatprove_spark__report.adb b/spark2014/patches/patch-src_gnatprove_spark__report.adb
deleted file mode 100644
index 63805166a6..0000000000
--- a/spark2014/patches/patch-src_gnatprove_spark__report.adb
+++ /dev/null
@@ -1,14 +0,0 @@
-$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
-@@ -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
deleted file mode 100644
index 2913f72ba1..0000000000
--- a/spark2014/patches/patch-why3_Makefile.in
+++ /dev/null
@@ -1,15 +0,0 @@
-$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
-@@ -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/xmlada/DESCR b/xmlada/DESCR
deleted file mode 100644
index 84345ffa3a..0000000000
--- a/xmlada/DESCR
+++ /dev/null
@@ -1,4 +0,0 @@
-XML/Ada: An XML parser for Ada95
-
-See the XML/Ada user's guide for information on how to use this library.
-This package includes static libraries only.
diff --git a/xmlada/Makefile b/xmlada/Makefile
deleted file mode 100644
index 2bc3bea6f2..0000000000
--- a/xmlada/Makefile
+++ /dev/null
@@ -1,46 +0,0 @@
-# $NetBSD: Makefile,v 1.0 2024/05/06 15:00:00 dkazankov Exp $
-
-DISTNAME= xmlada-${PKGVERSION_NOREV}
-PKGNAME= xmlada-25.0.0
-CATEGORIES= textproc devel
-MASTER_SITES= ${MASTER_SITE_GITHUB:=AdaCore/}
-GITHUB_PROJECT= xmlada
-GITHUB_TAG= v${PKGVERSION_NOREV}
-
-MAINTAINER= dkazankov%NetBSD.org@localhost
-HOMEPAGE= https://github.com/AdaCore/xmlada
-COMMENT= XML/Ada: An XML parser for Ada95
-LICENSE= gnu-gpl-v3
-
-USE_TOOLS+= gmake
-GNU_CONFIGURE= yes
-
-USE_LANGUAGES= ada
-GCC_REQD+= 13
-
-USE_GCC_RUNTIME= yes
-
-.include "../../mk/bsd.prefs.mk"
-
-SUBST_CLASSES+= fixver
-SUBST_STAGE.fixver= pre-configure
-SUBST_FILES.fixver= ./configure.in ./configure
-SUBST_MESSAGE.fixver= Fix version in configure
-SUBST_SED.fixver= -e 's,18.0w,25.0w,g'
-
-CONFIGURE_ARGS+= --exec-prefix=${PREFIX}
-
-USE_PKGSRC_GCC_RUNTIME?= no
-.if ${USE_PKGSRC_GCC_RUNTIME:tl} == "yes"
-CONFIGURE_ARGS+= --enable-shared
-.else
-CONFIGURE_ARGS+= --disable-shared
-.endif
-
-GENERATE_PLIST+= \
- cd ${DESTDIR}${PREFIX} && \
- ${FIND} include lib share \( -type f -or -type l \) -print | ${SORT};
-
-.include "../../devel/gprbuild/buildlink3.mk"
-
-.include "../../mk/bsd.pkg.mk"
diff --git a/xmlada/buildlink3.mk b/xmlada/buildlink3.mk
deleted file mode 100644
index bdcd13ce59..0000000000
--- a/xmlada/buildlink3.mk
+++ /dev/null
@@ -1,21 +0,0 @@
-# $NetBSD: buildlink3.mk,v 1.0 2024/05/06 16:00:00 dkazankov Exp $
-
-BUILDLINK_TREE+= xmlada
-
-.if !defined(XMLADA_BUILDLINK3_MK)
-XMLADA_BUILDLINK3_MK:=
-
-BUILDLINK_API_DEPENDS.xmlada+= xmlada>=24.0.0
-BUILDLINK_ABI_DEPENDS.xmlada+= xmlada>=25.0.0
-BUILDLINK_PKGSRCDIR.xmlada?= ../../wip/xmlada
-BUILDLINK_DEPMETHOD.xmlada?= build
-
-BUILDLINK_CONTENTS_FILTER.xmlada= \
- ${EGREP} '(include/.*\.ad.$$|lib/.*\.ali$$|lib/.*\.a$$|lib/.*\.so.*$$|share/gpr/manifests/.*|share/gpr/.*\.gpr$$)'
-
-pkgbase := xmlada
-.include "../../mk/pkg-build-options.mk"
-
-.endif
-
-BUILDLINK_TREE+= -xmlada
diff --git a/xmlada/distinfo b/xmlada/distinfo
deleted file mode 100644
index 6a64c048e5..0000000000
--- a/xmlada/distinfo
+++ /dev/null
@@ -1,6 +0,0 @@
-$NetBSD$
-
-BLAKE2s (xmlada-25.0.0.tar.gz) = c7e2b06977998dadbde002a6b80a75d3921860f20946c02a983a2048ade6e987
-SHA512 (xmlada-25.0.0.tar.gz) = c57db78e3afd20862c3275d3d0874ada1748e98df06a76841cb3dca3686b29c7693835a591ca5789dca2d3d6ba9677c9082df94857e180e0758a5b77fafc40c0
-Size (xmlada-25.0.0.tar.gz) = 1082553 bytes
-SHA1 (patch-configure) = abb1e41b3b5bb7ec67a9cf06a353926334623d67
diff --git a/xmlada/patches/patch-configure b/xmlada/patches/patch-configure
deleted file mode 100644
index 6ee4df821a..0000000000
--- a/xmlada/patches/patch-configure
+++ /dev/null
@@ -1,15 +0,0 @@
-$NetBSD: patch-configure,v 1.0 2024/05/14 13:00:00 dkazankov Exp $
-
-Fix cross compiling test
-
---- configure.orig 2023-09-07 14:33:41.000000000 +0300
-+++ configure
-@@ -1895,7 +1895,7 @@
- end Lib;
- EOF
-
-- if test "x$host_alias" != "x$target_alias"; then
-+ if test "x$host_alias" != "x$target_alias" && test "x" != "x$target_alias"; then
- $gprbuild --target=$target_alias -c -q -P$tmp/lib 2>/dev/null
- else
- $gprbuild -c -q -P$tmp/lib 2>/dev/null
Home |
Main Index |
Thread Index |
Old Index