cpet/freebsd-ports
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

math/why3-gpl: upgrade version 2014 => 2015

Browse Source 
While here, decouple this port from math/why3.  They are diverging fast.
This port is needed to build SPARK 2015 binaries which will be installed
by the lang/spark port (rather than building from source)
This commit is contained in:
John Marino 2015-06-26 22:13:46 +00:00
parent 9d8944598b
commit 80ccba4850
Notes: svn2git 2021-03-31 03:12:20 +00:00 
svn path=/head/; revision=390670
5 changed files with 90 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
math/why3-gpl/Makefile
View File

@ -2,21 +2,47 @@
# $FreeBSD$
PORTNAME= why3
PORTVERSION= 2014
PORTREVISION= 1
PORTVERSION= 2015
CATEGORIES= math
MASTER_SITES= http://downloads.dragonlace.net/src/ \
LOCAL/marino
PKGNAMESUFFIX= -gpl
DISTNAME= ${PORTNAME}${PKGNAMESUFFIX}-${PORTVERSION}-src
DISTNAME= why3-for-spark-gpl-${PORTVERSION}-src
MAINTAINER= marino@FreeBSD.org
COMMENT= Component of SPARK 2014
COMMENT= Component of SPARK 2015
LICENSE= LGPL21 GPLv3
LICENSE_COMB= multi
ALL_TARGET= all
BUILD_DEPENDS= menhir:${PORTSDIR}/devel/menhir \
ocaml-zip>1:${PORTSDIR}/archivers/ocaml-zip \
ocaml-zarith>1.2:${PORTSDIR}/math/ocaml-zarith \
lablgtk2:${PORTSDIR}/x11-toolkits/ocaml-lablgtk2 \
ocaml-sqlite3>2:${PORTSDIR}/databases/ocaml-sqlite3 \
ocaml-ocamlgraph>1.8:${PORTSDIR}/math/ocaml-ocamlgraph \
camlp5o:${PORTSDIR}/devel/ocaml-camlp5
USES= gmake
USE_OCAML= yes
ALL_TARGET= all
GNU_CONFIGURE= yes
INSTALL_TARGET= install-all
MAKE_JOBS_UNSAFE= yes
CONFIGURE_ARGS= --enable-relocation \
--disable-doc \
--disable-pvs-libs \
--disable-profiling \
--disable-coq-tactic \
--disable-coq-libs \
--disable-isabelle-libs
post-patch:
@${REINPLACE_CMD} -e 's|/bin/bash|/bin/sh|g' \
${WRKSRC}/src/util/sysutil.ml
@${REINPLACE_CMD} -e '/cp -f share\/Make/d' \
-e 's|why3.el|why3-mode.el|' ${WRKSRC}/Makefile.in
.include "${.CURDIR}/../why3/Makefile.common"
.include <bsd.port.mk>

4
math/why3-gpl/distinfo
View File

@ -1,2 +1,2 @@
SHA256 (why3-gpl-2014-src.tar.gz) = 0f598327b3c27f98bc7064929d990d422303155d106b1d9eb48246c039415e9e
SIZE (why3-gpl-2014-src.tar.gz) = 4568701
SHA256 (why3-for-spark-gpl-2015-src.tar.gz) = 90faf6001e4a9d9ccb7c913df8a2316bef004aaf9546a9a5ff6b08c28ff74ede
SIZE (why3-for-spark-gpl-2015-src.tar.gz) = 6880072

20
math/why3-gpl/files/patch-Makefile.in
View File

@ -1,6 +1,6 @@
--- Makefile.in.orig 2014-04-03 10:14:03.000000000 +0000
--- Makefile.in.orig 2015-06-26 21:21:27 UTC
+++ Makefile.in
@@ -46,7 +46,6 @@ OCAMLLIB = @OCAMLLIB@
@@ -45,7 +45,6 @@ OCAMLLIB = @OCAMLLIB@
OCAMLINSTALLLIB = $(DESTDIR)@OCAMLINSTALLLIB@
OCAMLBEST = @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
@ -8,3 +8,19 @@
COQC = @COQC@
COQDEP = @COQDEP@
CAMLP5O = @CAMLP5O@
@@ -638,12 +637,12 @@ SERVER_O:= $(addprefix src/tools/, $(add
opt: bin/why3server$(EXE)
bin/why3server$(EXE): $(SERVER_O)
- gcc -o $@ $^
+ $(CC) -o $@ $^
%.o: %.c %.h
- gcc -c -Wall -g -o $@ $<
+ $(CC) -c -Wall -g -o $@ $<
%.o: %.c
- gcc -c -Wall -g -o $@ $<
+ $(CC) -c -Wall -g -o $@ $<
src/tools/main.o:: src/tools/server-unix.c src/tools/server-win.c

6
math/why3-gpl/files/patch-src_tools_cpulimit.c
View File

@ -1,8 +1,8 @@
--- src/tools/cpulimit.c.orig 2014-03-14 15:01:03.000000000 +0000
--- src/tools/cpulimit.c.orig 2015-05-06 10:55:30 UTC
+++ src/tools/cpulimit.c
@@ -18,6 +18,7 @@
#include <stdlib.h>
@@ -19,6 +19,7 @@
#include <unistd.h>
#include <signal.h>
#include <errno.h>
+#include <signal.h>
#include <string.h>

49
math/why3-gpl/pkg-plist
View File

@ -1,33 +1,37 @@
bin/gnatwhy3
bin/why3
bin/why3-cpulimit
bin/why3bench
bin/why3config
bin/why3doc
bin/why3ide
bin/why3replayer
bin/why3session
bin/why3server
%%OCAML_SITELIBDIR%%/why3/META
%%OCAML_SITELIBDIR%%/why3/why3.a
%%OCAML_SITELIBDIR%%/why3/why3.cmi
%%OCAML_SITELIBDIR%%/why3/why3.cmx
%%OCAML_SITELIBDIR%%/why3/why3.cmxa
%%OCAML_SITELIBDIR%%/why3/why3.o
%%OCAML_SITELIBDIR%%/why3/why3extract.a
%%OCAML_SITELIBDIR%%/why3/why3extract.cmi
%%OCAML_SITELIBDIR%%/why3/why3extract.cmx
%%OCAML_SITELIBDIR%%/why3/why3extract.cmxa
%%OCAML_SITELIBDIR%%/why3/why3extract.o
lib/why3/commands/why3config
lib/why3/commands/why3doc
lib/why3/commands/why3execute
lib/why3/commands/why3extract
lib/why3/commands/why3ide
lib/why3/commands/why3prove
lib/why3/commands/why3realize
lib/why3/commands/why3replay
lib/why3/commands/why3session
lib/why3/commands/why3wc
lib/why3/plugins/dimacs.cmxs
lib/why3/plugins/genequlin.cmxs
lib/why3/plugins/hypothesis_selection.cmxs
lib/why3/plugins/tptp.cmxs
lib/why3/why3-call-pvs
share/emacs/site-lisp/why3.el
%%DATADIR%%/LICENSE
%%DATADIR%%/drivers/alt_ergo.drv
%%DATADIR%%/drivers/alt_ergo_0.92.drv
%%DATADIR%%/drivers/alt_ergo_0.93.drv
%%DATADIR%%/drivers/alt_ergo_0.94.drv
%%DATADIR%%/drivers/alt_ergo_bare.drv
%%DATADIR%%/drivers/alt_ergo_common.drv
%%DATADIR%%/drivers/alt_ergo_model.drv
%%DATADIR%%/drivers/alt_ergo_smt2.drv
%%DATADIR%%/drivers/beagle.drv
@ -35,11 +39,13 @@ lib/why3/why3-call-pvs
%%DATADIR%%/drivers/coq-realizations.aux
%%DATADIR%%/drivers/coq-realize.drv
%%DATADIR%%/drivers/coq.drv
%%DATADIR%%/drivers/coq_8_4.drv
%%DATADIR%%/drivers/cvc3.drv
%%DATADIR%%/drivers/cvc3_bare.drv
%%DATADIR%%/drivers/cvc4.drv
%%DATADIR%%/drivers/cvc4_14.drv
%%DATADIR%%/drivers/cvc4_15.drv
%%DATADIR%%/drivers/cvc4_bare.drv
%%DATADIR%%/drivers/cvc4_bv.gen
%%DATADIR%%/drivers/cvc4_gnatprove.drv
%%DATADIR%%/drivers/discrimination.gen
%%DATADIR%%/drivers/eprover.drv
@ -54,14 +60,19 @@ lib/why3/why3-call-pvs
%%DATADIR%%/drivers/metis.drv
%%DATADIR%%/drivers/metitarski.drv
%%DATADIR%%/drivers/ocaml-gen.drv
%%DATADIR%%/drivers/ocaml-no-arith.drv
%%DATADIR%%/drivers/ocaml-unsafe-int.drv
%%DATADIR%%/drivers/ocaml32.drv
%%DATADIR%%/drivers/ocaml64.drv
%%DATADIR%%/drivers/princess.drv
%%DATADIR%%/drivers/psyche.drv
%%DATADIR%%/drivers/pvs-common.gen
%%DATADIR%%/drivers/pvs-realizations.aux
%%DATADIR%%/drivers/pvs-realize.drv
%%DATADIR%%/drivers/pvs.drv
%%DATADIR%%/drivers/simplify.drv
%%DATADIR%%/drivers/smt-libv2-bv.gen
%%DATADIR%%/drivers/smt-libv2.drv
%%DATADIR%%/drivers/spass.drv
%%DATADIR%%/drivers/spass_types.drv
%%DATADIR%%/drivers/tptp-tff0.drv
@ -72,13 +83,13 @@ lib/why3/why3-call-pvs
%%DATADIR%%/drivers/why3.drv
%%DATADIR%%/drivers/why3_smt.drv
%%DATADIR%%/drivers/why3_tptp.drv
%%DATADIR%%/drivers/yices-smt2.drv
%%DATADIR%%/drivers/yices.drv
%%DATADIR%%/drivers/yices_bare.drv
%%DATADIR%%/drivers/z3.drv
%%DATADIR%%/drivers/z3_bare.drv
%%DATADIR%%/drivers/z3_432.drv
%%DATADIR%%/drivers/z3_smtv1.drv
%%DATADIR%%/drivers/zenon.drv
%%DATADIR%%/emacs/why3-mode.el
%%DATADIR%%/images/boomy/accept32.png
%%DATADIR%%/images/boomy/bug32.png
%%DATADIR%%/images/boomy/clock32.png
@ -94,6 +105,7 @@ lib/why3/why3-call-pvs
%%DATADIR%%/images/boomy/folder16.png
%%DATADIR%%/images/boomy/folder32.png
%%DATADIR%%/images/boomy/help32.png
%%DATADIR%%/images/boomy/license.txt
%%DATADIR%%/images/boomy/movefile32.png
%%DATADIR%%/images/boomy/obsaccept32.png
%%DATADIR%%/images/boomy/obsbug32.png
@ -114,6 +126,7 @@ lib/why3/why3-call-pvs
%%DATADIR%%/images/fatcow/accept.png
%%DATADIR%%/images/fatcow/bin.png
%%DATADIR%%/images/fatcow/bomb.png
%%DATADIR%%/images/fatcow/brick_delete.png
%%DATADIR%%/images/fatcow/bullet_black.png
%%DATADIR%%/images/fatcow/bullet_blue.png
%%DATADIR%%/images/fatcow/bullet_green.png
@ -122,6 +135,7 @@ lib/why3/why3-call-pvs
%%DATADIR%%/images/fatcow/cancel.png
%%DATADIR%%/images/fatcow/control_pause_blue.png
%%DATADIR%%/images/fatcow/control_play_blue.png
%%DATADIR%%/images/fatcow/database_delete.png
%%DATADIR%%/images/fatcow/ddr_memory.png
%%DATADIR%%/images/fatcow/delete.png
%%DATADIR%%/images/fatcow/exclamation.png
@ -131,7 +145,9 @@ lib/why3/why3-call-pvs
%%DATADIR%%/images/fatcow/multitool.png
%%DATADIR%%/images/fatcow/package.png
%%DATADIR%%/images/fatcow/pencil.png
%%DATADIR%%/images/fatcow/readme-fatcow.txt
%%DATADIR%%/images/fatcow/script.png
%%DATADIR%%/images/fatcow/time_delete.png
%%DATADIR%%/images/fatcow/timeline.png
%%DATADIR%%/images/fatcow/update.png
%%DATADIR%%/images/icons.rc
@ -146,11 +162,16 @@ lib/why3/why3-call-pvs
%%DATADIR%%/javascript/themes/default/throbber.gif
%%DATADIR%%/lang/why3.lang
%%DATADIR%%/modules/array.mlw
%%DATADIR%%/modules/bv.mlw
%%DATADIR%%/modules/hashtbl.mlw
%%DATADIR%%/modules/impset.mlw
%%DATADIR%%/modules/io.mlw
%%DATADIR%%/modules/mach/array.mlw
%%DATADIR%%/modules/mach/int.mlw
%%DATADIR%%/modules/mach/onetime.mlw
%%DATADIR%%/modules/mach/peano.mlw
%%DATADIR%%/modules/matrix.mlw
%%DATADIR%%/modules/null.mlw
%%DATADIR%%/modules/pqueue.mlw
%%DATADIR%%/modules/queue.mlw
%%DATADIR%%/modules/random.mlw
@ -162,7 +183,6 @@ lib/why3/why3-call-pvs
%%DATADIR%%/theories/bag.why
%%DATADIR%%/theories/bintree.why
%%DATADIR%%/theories/bool.why
%%DATADIR%%/theories/comparison.why
%%DATADIR%%/theories/floating_point.why
%%DATADIR%%/theories/function.why
%%DATADIR%%/theories/graph.why
@ -175,6 +195,7 @@ lib/why3/why3-call-pvs
%%DATADIR%%/theories/real.why
%%DATADIR%%/theories/regexp.why
%%DATADIR%%/theories/relations.why
%%DATADIR%%/theories/seq.why
%%DATADIR%%/theories/set.why
%%DATADIR%%/theories/sum.why
%%DATADIR%%/theories/tptp.why