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