pkgsrc-Changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
CVS commit: pkgsrc/devel
Module Name: pkgsrc
Committed By: dkazankov
Date: Mon Jul 28 06:52:41 UTC 2025
Modified Files:
pkgsrc/devel: Makefile
Added Files:
pkgsrc/devel/ada-sparklib-14: DESCR Makefile PLIST buildlink3.mk
distinfo
Log Message:
devel/ada-sparklib-14: add new package 14.0.0
SPARKlib contains various libraries, such as a wide range of containers,
as well as lemmas to use directly in user code.
To generate a diff of this commit:
cvs rdiff -u -r1.4494 -r1.4495 pkgsrc/devel/Makefile
cvs rdiff -u -r0 -r1.1 pkgsrc/devel/ada-sparklib-14/DESCR \
pkgsrc/devel/ada-sparklib-14/Makefile pkgsrc/devel/ada-sparklib-14/PLIST \
pkgsrc/devel/ada-sparklib-14/buildlink3.mk \
pkgsrc/devel/ada-sparklib-14/distinfo
Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.
Modified files:
Index: pkgsrc/devel/Makefile
diff -u pkgsrc/devel/Makefile:1.4494 pkgsrc/devel/Makefile:1.4495
--- pkgsrc/devel/Makefile:1.4494 Mon Jul 28 05:46:26 2025
+++ pkgsrc/devel/Makefile Mon Jul 28 06:52:41 2025
@@ -1,4 +1,4 @@
-# $NetBSD: Makefile,v 1.4494 2025/07/28 05:46:26 dkazankov Exp $
+# $NetBSD: Makefile,v 1.4495 2025/07/28 06:52:41 dkazankov Exp $
#
COMMENT= Development utilities
@@ -134,6 +134,7 @@ SUBDIR+= ada-gnatcoll-core-25
SUBDIR+= ada-libgpr-24
SUBDIR+= ada-libgpr-25
SUBDIR+= ada-libgpr2-25
+SUBDIR+= ada-sparklib-14
SUBDIR+= ade
SUBDIR+= adocman
SUBDIR+= aegis
Added files:
Index: pkgsrc/devel/ada-sparklib-14/DESCR
diff -u /dev/null pkgsrc/devel/ada-sparklib-14/DESCR:1.1
--- /dev/null Mon Jul 28 06:52:41 2025
+++ pkgsrc/devel/ada-sparklib-14/DESCR Mon Jul 28 06:52:41 2025
@@ -0,0 +1,6 @@
+SPARKlib libraries
+
+SPARKlib is meant to provide users of SPARK libraries to
+use in SPARK code. SPARKlib contains various libraries,
+such as a wide range of containers, as well as lemmas to
+use directly in user code.
\ No newline at end of file
Index: pkgsrc/devel/ada-sparklib-14/Makefile
diff -u /dev/null pkgsrc/devel/ada-sparklib-14/Makefile:1.1
--- /dev/null Mon Jul 28 06:52:41 2025
+++ pkgsrc/devel/ada-sparklib-14/Makefile Mon Jul 28 06:52:41 2025
@@ -0,0 +1,38 @@
+# $NetBSD: Makefile,v 1.1 2025/07/28 06:52:41 dkazankov Exp $
+
+DISTNAME= ${GITHUB_PROJECT}-fsf-14
+PKGNAME= sparklib-14-14.0.0
+CATEGORIES= devel
+MASTER_SITES= ${MASTER_SITE_GITHUB:=AdaCore/}
+GITHUB_PROJECT= SPARKlib
+GITHUB_TAG= fsf-14
+DISTFILES= ${DEFAULT_DISTFILES}
+
+MAINTAINER= dkazankov%NetBSD.org@localhost
+HOMEPAGE= https://github.com/AdaCore/SPARKlib
+COMMENT= SPARKlib libraries, FSF release 14
+LICENSE= apache-2.0
+
+USE_LANGUAGES= c ada
+
+USE_TOOLS+= gmake gsed
+
+.include "../../mk/bsd.prefs.mk"
+
+GCC_REQD+= 14
+
+BUILD_TARGET= generate
+
+do-install:
+ ${RUN} cd ${WRKSRC} && \
+ ${MKDIR} ${DESTDIR}${GNAT_PREFIX}/include/spark && \
+ ${MKDIR} ${DESTDIR}${GNAT_PREFIX}/lib/gnat && \
+ ${CP} -pr src/*.ad? ${DESTDIR}${GNAT_PREFIX}/include/spark && \
+ ${CP} -pr *.gpr ${DESTDIR}${GNAT_PREFIX}/lib/gnat && \
+ ${CP} -pr proof ${DESTDIR}${GNAT_PREFIX}/lib/gnat
+
+GENERATE_PLIST+= \
+ cd ${DESTDIR}${PREFIX} && \
+ ${FIND} ${GNAT_PKGBASE} \( -type f -or -type l \) -print | ${SORT};
+
+.include "../../mk/bsd.pkg.mk"
Index: pkgsrc/devel/ada-sparklib-14/PLIST
diff -u /dev/null pkgsrc/devel/ada-sparklib-14/PLIST:1.1
--- /dev/null Mon Jul 28 06:52:41 2025
+++ pkgsrc/devel/ada-sparklib-14/PLIST Mon Jul 28 06:52:41 2025
@@ -0,0 +1,303 @@
+@comment $NetBSD: PLIST,v 1.1 2025/07/28 06:52:41 dkazankov Exp $
+${GNAT_PKGBASE}/include/spark/spark-big_integers.ads
+${GNAT_PKGBASE}/include/spark/spark-big_integers__light.ads
+${GNAT_PKGBASE}/include/spark/spark-big_intervals.ads
+${GNAT_PKGBASE}/include/spark/spark-big_intervals__light.ads
+${GNAT_PKGBASE}/include/spark/spark-big_reals.ads
+${GNAT_PKGBASE}/include/spark/spark-big_reals__light.adb
+${GNAT_PKGBASE}/include/spark/spark-big_reals__light.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-doubly_linked_lists.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-doubly_linked_lists.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-hashed_maps.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-hashed_maps.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-hashed_sets.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-hashed_sets.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-holders.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-holders.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-ordered_maps.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-ordered_maps.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-ordered_sets.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-ordered_sets.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-unbounded_doubly_linked_lists.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-unbounded_doubly_linked_lists.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-unbounded_hashed_maps.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-unbounded_hashed_maps.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-unbounded_hashed_sets.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-unbounded_hashed_sets.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-unbounded_ordered_maps.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-unbounded_ordered_maps.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-unbounded_ordered_sets.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-unbounded_ordered_sets.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-unbounded_vectors.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-unbounded_vectors.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-vectors.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-formal-vectors.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-formal.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-base.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-base.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-infinite_sequences-higher_order.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-infinite_sequences-higher_order.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-infinite_sequences.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-infinite_sequences.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-infinite_sequences__light.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-infinite_sequences__light.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-maps-higher_order.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-maps-higher_order.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-maps.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-maps.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-maps__light.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-maps__light.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-multisets.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-multisets.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-multisets__light.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-multisets__light.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-sets-higher_order.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-sets-higher_order.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-sets.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-sets.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-sets__light.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-sets__light.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-vectors-higher_order.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-vectors-higher_order.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-vectors.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-vectors.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-vectors__light.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-functional-vectors__light.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-functional.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-parameter_checks.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-parameter_checks.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-stable_sorting.adb
+${GNAT_PKGBASE}/include/spark/spark-containers-stable_sorting.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-types.ads
+${GNAT_PKGBASE}/include/spark/spark-containers-types__light.ads
+${GNAT_PKGBASE}/include/spark/spark-containers.ads
+${GNAT_PKGBASE}/include/spark/spark-containers__exec.ads
+${GNAT_PKGBASE}/include/spark/spark-conversions-float_conversions.ads
+${GNAT_PKGBASE}/include/spark/spark-conversions-long_float_conversions.ads
+${GNAT_PKGBASE}/include/spark/spark-conversions-long_integer_conversions.ads
+${GNAT_PKGBASE}/include/spark/spark-conversions.ads
+${GNAT_PKGBASE}/include/spark/spark-cut_operations.adb
+${GNAT_PKGBASE}/include/spark/spark-cut_operations.ads
+${GNAT_PKGBASE}/include/spark/spark-higher_order-fold.adb
+${GNAT_PKGBASE}/include/spark/spark-higher_order-fold.ads
+${GNAT_PKGBASE}/include/spark/spark-higher_order.adb
+${GNAT_PKGBASE}/include/spark/spark-higher_order.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas-arithmetic.adb
+${GNAT_PKGBASE}/include/spark/spark-lemmas-arithmetic.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas-constrained_array.adb
+${GNAT_PKGBASE}/include/spark/spark-lemmas-constrained_array.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas-fixed_point_arithmetic.adb
+${GNAT_PKGBASE}/include/spark/spark-lemmas-fixed_point_arithmetic.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas-float_arithmetic.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas-float_base.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas-floating_point_arithmetic.adb
+${GNAT_PKGBASE}/include/spark/spark-lemmas-floating_point_arithmetic.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas-integer_arithmetic.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas-long_float_arithmetic.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas-long_integer_arithmetic.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas-mod32_arithmetic.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas-mod64_arithmetic.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas-mod_arithmetic.adb
+${GNAT_PKGBASE}/include/spark/spark-lemmas-mod_arithmetic.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas-unconstrained_array.adb
+${GNAT_PKGBASE}/include/spark/spark-lemmas-unconstrained_array.ads
+${GNAT_PKGBASE}/include/spark/spark-lemmas.ads
+${GNAT_PKGBASE}/include/spark/spark-pointers-abstract_maps.ads
+${GNAT_PKGBASE}/include/spark/spark-pointers-abstract_sets.adb
+${GNAT_PKGBASE}/include/spark/spark-pointers-abstract_sets.ads
+${GNAT_PKGBASE}/include/spark/spark-pointers-pointers_with_aliasing.adb
+${GNAT_PKGBASE}/include/spark/spark-pointers-pointers_with_aliasing.ads
+${GNAT_PKGBASE}/include/spark/spark-pointers-pointers_with_aliasing_separate_memory.adb
+${GNAT_PKGBASE}/include/spark/spark-pointers-pointers_with_aliasing_separate_memory.ads
+${GNAT_PKGBASE}/include/spark/spark-pointers.ads
+${GNAT_PKGBASE}/include/spark/spark-tests-array_lemmas.adb
+${GNAT_PKGBASE}/include/spark/spark-tests-array_lemmas.ads
+${GNAT_PKGBASE}/include/spark/spark-tests.ads
+${GNAT_PKGBASE}/include/spark/spark.ads
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_is_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_div_right_negative_is_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_by_less_than_one__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_float_arithmetic__lemma_mult_right_negative_is_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_exp_is_monotonic__pragargs__call_Ole.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__long_integer_arithmetic__lemma_mod_symmetry__pragargs__call_Oeq.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_is_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_protect__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_protect__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_scale__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_scale__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod32_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_is_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_is_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_div_then_mult_bounds__pragargs__cmp1.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_is_strictly_monotonic__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_protect__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_protect__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_scale__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_scale__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_div_is_ident__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__lemmas__mod64_arithmetic__lemma_mult_then_mod_is_zero__pragargs__cmp.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__tests__array_lemmas__test_ufloat__lemma_transitive_order__pragargs__forall.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__tests__array_lemmas__test_ufloat__lemma_transitive_order__pragargs__forall.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__tests__array_lemmas__test_uint__lemma_transitive_order__pragargs__forall.ctx
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/Ada___ada___spark__tests__array_lemmas__test_uint__lemma_transitive_order__pragargs__forall.v
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/float32_div_common.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/float32_mul_common.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/float64_div_common.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/float64_mul_common.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/float_div_is_monotonic.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/float_div_right_negative_is_monotonic.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/float_mult_by_less_than_one.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/float_mult_is_monotonic.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/float_mult_right_negative_is_monotonic.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_exp_monotonic.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_mod_symmetry.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_modular_div_is_monotonic.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_modular_div_then_mult_bounds_part1.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_modular_div_then_mult_bounds_part2.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_modular_mult_is_monotonic.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_modular_mult_is_strictly_monotonic.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_modular_mult_protect.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_modular_mult_scale.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_modular_mult_then_div_is_ident.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_modular_mult_then_mod_is_zero.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_mult_protect.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_raising_order_float.prf
+${GNAT_PKGBASE}/lib/gnat/proof/Coq/common/lemma_raising_order_int.prf
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/040afe09a523c555222f-etic__lemma_mult_then_mod_is_zero/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/074951e582b42a4e86a3-__long_float_arithmetic__is_float/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/0d115cdeddec362ba5b0-test_uint__lemma_transitive_order/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/0eec99c81c556bec05d8-thmetic__lemma_rounding_error_mul/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/10d4c16efbd8aa8170b4-tic__lemma_mult_then_div_is_ident/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/1a869736986613d2894c-etic__lemma_mult_by_less_than_one/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/1bebbf763be867e613ea-lemmas__test_transitive_order_int/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/1e7136b07bae6812da3e-_lemma_mult_is_strictly_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/1ef388e82327ebe05e9b-rithmetic__lemma_div_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/1f0315da139ffdf3f46a-thmetic__lemma_rounding_error_add/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/2967a7190c1d6da72797-thmetic__lemma_rounding_error_mul/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/2acba862a25cb30487dd-rithmetic__lemma_exp_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/318da9314d00065ad977-ithmetic__lemma_mult_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/31b9a6b5a7821bc2e235-_lemma_mult_is_strictly_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/343ad5c090e48c5b5486-ithmetic__lemma_integer_mul_exact/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/394be94555b7a5bce5c2-ithmetic__lemma_mult_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/3dc15e949b92e6bc3e8c-thmetic__lemma_exp_is_monotonic_2/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/4068728d4e1ab489badc-eger_arithmetic__lemma_mult_scale/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/42257e019f886a53575b-etic__lemma_mult_then_mod_is_zero/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/46f26c24d6f307eefccb-tic__lemma_div_right_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/5087c1c41d1ea50f3b43-etic__lemma_div_left_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/51bc7cff3e9f5104ac8e-ithmetic__lemma_integer_add_exact/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/520af1b7421cc3173d6b-thmetic__lemma_rounding_error_add/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/55ea751b3442847e0a51-__float_arithmetic__is_integer_64/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/55f6cbcbdba2f08f95b8-ong_float_arithmetic__is_float__2/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/5684f1ac3b8758fec495-mas__test_transitive_order_int__2/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/599d2e5874b4d4973ca3-ithmetic__lemma_mult_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/60110fdb095a980207eb-er_arithmetic__lemma_mult_protect/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/6045d6e400b0ed266a82-rithmetic__lemma_div_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/6298a36c67bed51bcc6c-er_arithmetic__lemma_mod_symmetry/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/64bfaeb2e0dfd3d7848c-rithmetic__lemma_add_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/672f51d6643918282f3d-rithmetic__lemma_sub_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/689debb73baf8b61312d-etic__lemma_mult_by_less_than_one/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/79be5df150d5a95b881c-mas__float_arithmetic__is_integer/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/7b0c1771dc98feed9bdf-g_float_arithmetic__is_integer_32/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/7d58790d26e272271390-teger_arithmetic__lemma_mod_range/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/80af801f2bce867288a3-ithmetic__lemma_integer_mul_exact/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/856058dc67cf27cb38ef-teger_arithmetic__lemma_mod_range/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/8a46f225d0a415c477d1-tic__lemma_mult_then_div_is_ident/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/8b3edca72c143147c13c-od64_arithmetic__lemma_mult_scale/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/90139425da4995117a3e-thmetic__lemma_rounding_error_sub/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/90beef9de31d8c2ddd8c-64_arithmetic__lemma_mult_protect/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/93853065a2ed80673b26-er_arithmetic__lemma_mod_symmetry/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/95588777efc76a6aa91f-thmetic__lemma_rounding_error_div/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/9a2b1b428320ac4f0d30-od32_arithmetic__lemma_mult_scale/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/9bc0ca42f87caa33f66d-rithmetic__lemma_sub_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/9c7254124efb04d2e062-ithmetic__lemma_integer_add_exact/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/9c9e073d80b08d5889a7-metic__lemma_div_then_mult_bounds/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/a0a0414003f49a416a70-mmas__test_transitive_order_float/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/a1be8e7289746f2c938d-rithmetic__lemma_div_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/a3e25d9d28128ccba6e2-g_float_arithmetic__is_integer_64/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/a68b03e691bd98079629-er_arithmetic__lemma_mult_protect/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/a7d3de45647bc565d79c-st_ufloat__lemma_transitive_order/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/aa778117599e6dbefaf6-thmetic__lemma_rounding_error_sub/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/acb71b83cf3c5ff2746d-long_float_arithmetic__is_integer/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/ada___ada___spark__lemmas__float_arithmetic__is_float/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/ada___ada___spark__lemmas__long_float_arithmetic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/ada___spark__big_intervals__in_range/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/ada___spark__big_intervals__interval/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/ada___spark__big_intervals__next/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/ae7bcce82a34a7b72e89-etic__lemma_mult_then_mod_is_zero/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/af3c24809d6ba460433e-a_div_right_negative_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/af924488ea5f094ec958-a_div_right_negative_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/b3c56a894cb1cd064128-thmetic__lemma_rounding_error_div/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/b539d32b20872851a36f-ithmetic__lemma_mult_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/b73f1b059ec7ebcb16fb-_mult_right_negative_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/bc94551497e3edc0690a-tic__lemma_mult_then_div_is_ident/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/c2f4101d952e5f6797fe-metic__lemma_div_then_mult_bounds/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/c3139777773dfae02020-as__float_arithmetic__is_float__2/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/c57cc64d48915c7cf4c6-ithmetic__lemma_mult_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/c5c674ab02b37b6ebffd-s__test_transitive_order_float__2/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/c792e192cd78a54d2195-_lemma_mult_is_strictly_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/c952ff1888f9b88502f9-rithmetic__lemma_div_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/ca8899d1fe1cc264c072-__float_arithmetic__is_integer_32/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/d0ef2d7439290eb69571-_lemma_mult_is_strictly_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/d17bb852e0d1092e361d-etic__lemma_div_left_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/d6ca4205678e8f67e72c-rithmetic__lemma_exp_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/d9c64b991a89ace0ee39-32_arithmetic__lemma_mult_protect/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/da52b96556e8a5f7b3d4-ithmetic__lemma_integer_sub_exact/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/db72f67962265f3b2137-rithmetic__lemma_div_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/dfe0df76071bd3cbba92-etic__lemma_mult_then_mod_is_zero/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/e35fa81cbf0fd3d86c91-thmetic__lemma_exp_is_monotonic_2/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/e4e41c56561a343c1891-tic__lemma_div_right_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/e889c0b75746d40581a8-ithmetic__lemma_integer_sub_exact/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/eac46e7c965a06115d54-ithmetic__lemma_mult_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/f2c4ee31bfead0a3a396-tic__lemma_mult_then_div_is_ident/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/f6d237854fd3fbab4403-_mult_right_negative_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/f91d45a4a337c2e3996e-eger_arithmetic__lemma_mult_scale/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/ff8afdfddc7afbb29e8b-rithmetic__lemma_div_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/proof/sessions/ffc8b982ef83f179802f-rithmetic__lemma_add_is_monotonic/why3session.xml
+${GNAT_PKGBASE}/lib/gnat/sparklib.gpr
+${GNAT_PKGBASE}/lib/gnat/sparklib_common.gpr
+${GNAT_PKGBASE}/lib/gnat/sparklib_external.gpr
+${GNAT_PKGBASE}/lib/gnat/sparklib_light.gpr
+${GNAT_PKGBASE}/lib/gnat/sparklib_light_external.gpr
Index: pkgsrc/devel/ada-sparklib-14/buildlink3.mk
diff -u /dev/null pkgsrc/devel/ada-sparklib-14/buildlink3.mk:1.1
--- /dev/null Mon Jul 28 06:52:41 2025
+++ pkgsrc/devel/ada-sparklib-14/buildlink3.mk Mon Jul 28 06:52:41 2025
@@ -0,0 +1,19 @@
+# $NetBSD: buildlink3.mk,v 1.1 2025/07/28 06:52:41 dkazankov Exp $
+
+BUILDLINK_TREE+= sparklib-14
+
+.if !defined(SPARKLIB_14_BUILDLINK3_MK)
+SPARKLIB_14_BUILDLINK3_MK:=
+
+BUILDLINK_API_DEPENDS.sparklib-14+= sparklib-14>=14.0.0
+BUILDLINK_PKGSRCDIR.sparklib-14?= ../../devel/ada-sparklib-14
+BUILDLINK_DEPMETHOD.sparklib-14?= build
+
+BUILDLINK_CONTENTS_FILTER.sparklib-14= ${TRUE}
+
+BUILDLINK_FNAME_TRANSFORM.sparklib-14+= \
+ -e "s|${BUILDLINK_DIR}/${GNAT_PKGBASE}/|${BUILDLINK_DIR}/|g"
+
+.endif
+
+BUILDLINK_TREE+= -sparklib-14
Index: pkgsrc/devel/ada-sparklib-14/distinfo
diff -u /dev/null pkgsrc/devel/ada-sparklib-14/distinfo:1.1
--- /dev/null Mon Jul 28 06:52:41 2025
+++ pkgsrc/devel/ada-sparklib-14/distinfo Mon Jul 28 06:52:41 2025
@@ -0,0 +1,5 @@
+$NetBSD: distinfo,v 1.1 2025/07/28 06:52:41 dkazankov Exp $
+
+BLAKE2s (SPARKlib-fsf-14.tar.gz) = b1b62a533d681917108aa7ac9b70d052fb7760c7959492c1c36fbf1a14acf789
+SHA512 (SPARKlib-fsf-14.tar.gz) = 9e6f695a095deaad8bfa8f8348dbc089dec8c05f3ec18c662a91cf0d2c0d8a6aa7a644c83ef304cd0fdb7dc52220abcfd8f4171fb0fcf2411a679da398eeda6f
+Size (SPARKlib-fsf-14.tar.gz) = 349425 bytes
Home |
Main Index |
Thread Index |
Old Index