mirror of
https://git.freebsd.org/ports.git
synced 2025-05-31 10:26:28 -04:00
- Update coq to 8.4 pl1 [1]
http://coq.inria.fr/coq-84 - Remove local patch that is now included upstream - Add ocaml-findlib as build dependency PR: ports/176056 Submitted by: Jaap Boender <jaapb@kerguelen.org>
This commit is contained in:
Johan van Selst
parent
cb0287c3fd
commit
df999ac7da
Notes:
svn2git
2021-03-31 03:12:20 +00:00
svn path=/head/; revision=312410
4 changed files with 896 additions and 1194 deletions
|
|
@ -1,13 +1,8 @@
|
|||
# New ports collection makefile for: coq
|
||||
# Date created: 2004-10-11
|
||||
# Whom: Rene Ladan <r.c.ladan@student.tue.nl>
|
||||
#
|
||||
# Created by: Rene Ladan <r.c.ladan@student.tue.nl>
|
||||
# $FreeBSD$
|
||||
#
|
||||
|
||||
PORTNAME= coq
|
||||
PORTVERSION= 8.3.3
|
||||
PORTREVISION= 1
|
||||
PORTVERSION= 8.4.1
|
||||
PORTEPOCH= 1
|
||||
CATEGORIES= math
|
||||
MASTER_SITES= http://coq.inria.fr/distrib/V${COQVERSION}/files/ \
|
||||
|
|
@ -17,7 +12,8 @@ DISTNAME= ${PORTNAME}-${COQVERSION}
|
|||
MAINTAINER= johans@FreeBSD.org
|
||||
COMMENT= Theorem prover based on lambda-C
|
||||
|
||||
BUILD_DEPENDS= camlp5:${PORTSDIR}/devel/ocaml-camlp5
|
||||
BUILD_DEPENDS= camlp5:${PORTSDIR}/devel/ocaml-camlp5 \
|
||||
ocamlfind:${PORTSDIR}/devel/ocaml-findlib
|
||||
|
||||
COQVERSION= ${PORTVERSION:R}pl${PORTVERSION:E}
|
||||
USE_OCAML= yes
|
||||
|
|
@ -26,6 +22,7 @@ ALL_TARGET= world
|
|||
|
||||
HAS_CONFIGURE= yes
|
||||
CONFIGURE_ARGS= --prefix ${PREFIX}
|
||||
CONFIGURE_ARGS+=--mandir ${PREFIX}/man
|
||||
CONFIGURE_ARGS+=--emacslib ${PREFIX}/share/emacs/site-lisp
|
||||
CONFIGURE_ARGS+=--opt
|
||||
|
||||
|
|
|
|||
|
|
@ -1,2 +1,2 @@
|
|||
SHA256 (coq-8.3pl3.tar.gz) = af259e9a723761327137018fdc0b98ada71095ff033b9e169d175d92b9537947
|
||||
SIZE (coq-8.3pl3.tar.gz) = 3859883
|
||||
SHA256 (coq-8.4pl1.tar.gz) = 5d0e4553ab50677a94b4d5ca1650a90718e9362082a649ba95be4010390a0f80
|
||||
SIZE (coq-8.4pl1.tar.gz) = 4139808
|
||||
|
|
|
|||
|
|
@ -1,357 +0,0 @@
|
|||
Fix compilation with camlp5 6.05
|
||||
Patch from the official coq svn repository (revision 15025)
|
||||
|
||||
Index: checker/checker.ml
|
||||
===================================================================
|
||||
--- checker/checker.ml (revision 15024)
|
||||
+++ checker/checker.ml (revision 15025)
|
||||
@@ -274,7 +274,7 @@
|
||||
(* let ctx = Check.get_env() in
|
||||
hov 0
|
||||
(str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*)
|
||||
- | Stdpp.Exc_located (loc,exc) ->
|
||||
+ | Compat.Exc_located (loc,exc) ->
|
||||
hov 0 ((if loc = dummy_loc then (mt ())
|
||||
else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
|
||||
++ explain_exn exc)
|
||||
Index: lib/compat.ml4
|
||||
===================================================================
|
||||
--- lib/compat.ml4 (revision 15024)
|
||||
+++ lib/compat.ml4 (revision 15025)
|
||||
@@ -15,6 +15,7 @@
|
||||
IFDEF CAMLP5 THEN
|
||||
module M = struct
|
||||
type loc = Stdpp.location
|
||||
+exception Exc_located = Ploc.Exc
|
||||
let dummy_loc = Stdpp.dummy_loc
|
||||
let make_loc = Stdpp.make_loc
|
||||
let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc
|
||||
@@ -26,6 +27,7 @@
|
||||
end
|
||||
ELSE IFDEF OCAML308 THEN
|
||||
module M = struct
|
||||
+exception Exc_located = Stdpp.Exc_located
|
||||
type loc = Token.flocation
|
||||
let dummy_loc = Token.dummy_loc
|
||||
let make_loc loc = Token.make_loc loc
|
||||
@@ -45,6 +47,7 @@
|
||||
end
|
||||
ELSE
|
||||
module M = struct
|
||||
+exception Exc_located = Stdpp.Exc_located
|
||||
type loc = int * int
|
||||
let dummy_loc = (0,0)
|
||||
let make_loc x = x
|
||||
@@ -59,6 +62,7 @@
|
||||
END
|
||||
|
||||
type loc = M.loc
|
||||
+exception Exc_located = M.Exc_located
|
||||
let dummy_loc = M.dummy_loc
|
||||
let make_loc = M.make_loc
|
||||
let unloc = M.unloc
|
||||
Index: pretyping/pretype_errors.ml
|
||||
===================================================================
|
||||
--- pretyping/pretype_errors.ml (revision 15024)
|
||||
+++ pretyping/pretype_errors.ml (revision 15025)
|
||||
@@ -45,7 +45,7 @@
|
||||
|
||||
let precatchable_exception = function
|
||||
| Util.UserError _ | TypeError _ | PretypeError _
|
||||
- | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ |
|
||||
+ | Compat.Exc_located(_,(Util.UserError _ | TypeError _ |
|
||||
Nametab.GlobalizationError _ | PretypeError _)) -> true
|
||||
| _ -> false
|
||||
|
||||
Index: pretyping/cases.ml
|
||||
===================================================================
|
||||
--- pretyping/cases.ml (revision 15024)
|
||||
+++ pretyping/cases.ml (revision 15025)
|
||||
@@ -100,7 +100,7 @@
|
||||
| h::t ->
|
||||
try f h
|
||||
with UserError _ | TypeError _ | PretypeError _
|
||||
- | Stdpp.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
|
||||
+ | Compat.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) ->
|
||||
list_try_compile f t
|
||||
|
||||
let force_name =
|
||||
Index: pretyping/typeclasses_errors.ml
|
||||
===================================================================
|
||||
--- pretyping/typeclasses_errors.ml (revision 15024)
|
||||
+++ pretyping/typeclasses_errors.ml (revision 15025)
|
||||
@@ -47,7 +47,7 @@
|
||||
raise (TypeClassError (env, UnsatisfiableConstraints (evd, None)))
|
||||
| Some ev ->
|
||||
let loc, kind = Evd.evar_source ev evd in
|
||||
- raise (Stdpp.Exc_located (loc, TypeClassError
|
||||
+ raise (Compat.Exc_located (loc, TypeClassError
|
||||
(env, UnsatisfiableConstraints (evd, Some (ev, kind)))))
|
||||
|
||||
let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
|
||||
@@ -55,5 +55,5 @@
|
||||
let rec unsatisfiable_exception exn =
|
||||
match exn with
|
||||
| TypeClassError (_, UnsatisfiableConstraints _) -> true
|
||||
- | Stdpp.Exc_located(_, e) -> unsatisfiable_exception e
|
||||
+ | Compat.Exc_located(_, e) -> unsatisfiable_exception e
|
||||
| _ -> false
|
||||
Index: plugins/subtac/subtac_obligations.ml
|
||||
===================================================================
|
||||
--- plugins/subtac/subtac_obligations.ml (revision 15024)
|
||||
+++ plugins/subtac/subtac_obligations.ml (revision 15025)
|
||||
@@ -485,8 +485,8 @@
|
||||
true
|
||||
else false
|
||||
with
|
||||
- | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
|
||||
- | Stdpp.Exc_located(_, Refiner.FailError (_, s))
|
||||
+ | Compat.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
|
||||
+ | Compat.Exc_located(_, Refiner.FailError (_, s))
|
||||
| Refiner.FailError (_, s) ->
|
||||
user_err_loc (fst obl.obl_source, "solve_obligation", Lazy.force s)
|
||||
| e -> false
|
||||
Index: toplevel/cerrors.ml
|
||||
===================================================================
|
||||
--- toplevel/cerrors.ml (revision 15024)
|
||||
+++ toplevel/cerrors.ml (revision 15025)
|
||||
@@ -81,7 +81,7 @@
|
||||
hov 0 (str "Syntax error: Undefined token.")
|
||||
| Lexer.Error (Bad_token s) ->
|
||||
hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".")
|
||||
- | Stdpp.Exc_located (loc,exc) ->
|
||||
+ | Compat.Exc_located (loc,exc) ->
|
||||
hov 0 ((if loc = dummy_loc then (mt ())
|
||||
else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
|
||||
++ explain_exn_default_aux anomaly_string report_fn exc)
|
||||
@@ -156,8 +156,8 @@
|
||||
| Proof_type.LtacLocated (s,exc) ->
|
||||
EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()),
|
||||
Some (process_vernac_interp_error exc))
|
||||
- | Stdpp.Exc_located (loc,exc) ->
|
||||
- Stdpp.Exc_located (loc,process_vernac_interp_error exc)
|
||||
+ | Compat.Exc_located (loc,exc) ->
|
||||
+ Compat.Exc_located (loc,process_vernac_interp_error exc)
|
||||
| exc ->
|
||||
exc
|
||||
|
||||
Index: toplevel/vernac.ml
|
||||
===================================================================
|
||||
--- toplevel/vernac.ml (revision 15024)
|
||||
+++ toplevel/vernac.ml (revision 15025)
|
||||
@@ -41,14 +41,14 @@
|
||||
match re with
|
||||
| Error_in_file (_, (b,f,loc), e) when loc <> dummy_loc ->
|
||||
((b, f, loc), e)
|
||||
- | Stdpp.Exc_located (loc, e) when loc <> dummy_loc ->
|
||||
+ | Compat.Exc_located (loc, e) when loc <> dummy_loc ->
|
||||
((false,file, loc), e)
|
||||
- | Stdpp.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
|
||||
+ | Compat.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
|
||||
in
|
||||
raise (Error_in_file (file, inner, disable_drop inex))
|
||||
|
||||
let real_error = function
|
||||
- | Stdpp.Exc_located (_, e) -> e
|
||||
+ | Compat.Exc_located (_, e) -> e
|
||||
| Error_in_file (_, _, e) -> e
|
||||
| e -> e
|
||||
|
||||
Index: toplevel/toplevel.ml
|
||||
===================================================================
|
||||
--- toplevel/toplevel.ml (revision 15024)
|
||||
+++ toplevel/toplevel.ml (revision 15025)
|
||||
@@ -274,7 +274,7 @@
|
||||
let rec is_pervasive_exn = function
|
||||
| Out_of_memory | Stack_overflow | Sys.Break -> true
|
||||
| Error_in_file (_,_,e) -> is_pervasive_exn e
|
||||
- | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
|
||||
+ | Compat.Exc_located (_,e) -> is_pervasive_exn e
|
||||
| DuringCommandInterp (_,e) -> is_pervasive_exn e
|
||||
| _ -> false
|
||||
|
||||
@@ -290,7 +290,7 @@
|
||||
in
|
||||
let (locstrm,exc) =
|
||||
match exc with
|
||||
- | Stdpp.Exc_located (loc, ie) ->
|
||||
+ | Compat.Exc_located (loc, ie) ->
|
||||
if valid_buffer_loc top_buffer dloc loc then
|
||||
(print_highlight_location top_buffer loc, ie)
|
||||
else
|
||||
@@ -325,7 +325,7 @@
|
||||
let rec discard_to_dot () =
|
||||
try
|
||||
Gram.Entry.parse parse_to_dot top_buffer.tokens
|
||||
- with Stdpp.Exc_located(_,(Token.Error _|Lexer.Error _)) ->
|
||||
+ with Compat.Exc_located(_,(Token.Error _|Lexer.Error _)) ->
|
||||
discard_to_dot()
|
||||
|
||||
|
||||
Index: tactics/extratactics.ml4
|
||||
===================================================================
|
||||
--- tactics/extratactics.ml4 (revision 15024)
|
||||
+++ tactics/extratactics.ml4 (revision 15025)
|
||||
@@ -580,7 +580,7 @@
|
||||
try
|
||||
Pretyping.Default.understand sigma env t_hole
|
||||
with
|
||||
- | Stdpp.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
|
||||
+ | Compat.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
|
||||
resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole)
|
||||
in
|
||||
let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
|
||||
Index: tactics/class_tactics.ml4
|
||||
===================================================================
|
||||
--- tactics/class_tactics.ml4 (revision 15024)
|
||||
+++ tactics/class_tactics.ml4 (revision 15025)
|
||||
@@ -219,7 +219,7 @@
|
||||
|
||||
let rec catchable = function
|
||||
| Refiner.FailError _ -> true
|
||||
- | Stdpp.Exc_located (_, e) -> catchable e
|
||||
+ | Compat.Exc_located (_, e) -> catchable e
|
||||
| e -> Logic.catchable_exception e
|
||||
|
||||
let is_dep gl gls =
|
||||
Index: tactics/rewrite.ml4
|
||||
===================================================================
|
||||
--- tactics/rewrite.ml4 (revision 15024)
|
||||
+++ tactics/rewrite.ml4 (revision 15025)
|
||||
@@ -1057,7 +1057,7 @@
|
||||
else tclIDTAC
|
||||
in tclTHENLIST [evartac; rewtac] gl
|
||||
with
|
||||
- | Stdpp.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
|
||||
+ | Compat.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
|
||||
| TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
|
||||
Refiner.tclFAIL_lazy 0
|
||||
(lazy (str"setoid rewrite failed: unable to satisfy the rewriting constraints."
|
||||
Index: tactics/tacinterp.ml
|
||||
===================================================================
|
||||
--- tactics/tacinterp.ml (revision 15024)
|
||||
+++ tactics/tacinterp.ml (revision 15025)
|
||||
@@ -93,15 +93,15 @@
|
||||
let catch_error call_trace tac g =
|
||||
if call_trace = [] then tac g else try tac g with
|
||||
| LtacLocated _ as e -> raise e
|
||||
- | Stdpp.Exc_located (_,LtacLocated _) as e -> raise e
|
||||
+ | Compat.Exc_located (_,LtacLocated _) as e -> raise e
|
||||
| e ->
|
||||
let (nrep,loc',c),tail = list_sep_last call_trace in
|
||||
- let loc,e' = match e with Stdpp.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
|
||||
+ let loc,e' = match e with Compat.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
|
||||
if tail = [] then
|
||||
let loc = if loc = dloc then loc' else loc in
|
||||
- raise (Stdpp.Exc_located(loc,e'))
|
||||
+ raise (Compat.Exc_located(loc,e'))
|
||||
else
|
||||
- raise (Stdpp.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
|
||||
+ raise (Compat.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
|
||||
|
||||
(* Signature for interpretation: val_interp and interpretation functions *)
|
||||
type interp_sign =
|
||||
@@ -1979,14 +1979,14 @@
|
||||
VRTactic (catch_error trace tac goal)
|
||||
| a -> a)
|
||||
with
|
||||
- | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s))
|
||||
- | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
|
||||
+ | FailError (0,s) | Compat.Exc_located(_, FailError (0,s))
|
||||
+ | Compat.Exc_located(_,LtacLocated (_,FailError (0,s))) ->
|
||||
raise (Eval_fail (Lazy.force s))
|
||||
| FailError (lvl,s) -> raise (FailError (lvl - 1, s))
|
||||
- | Stdpp.Exc_located(s,FailError (lvl,s')) ->
|
||||
- raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
|
||||
- | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
|
||||
- raise (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s'))))
|
||||
+ | Compat.Exc_located(s,FailError (lvl,s')) ->
|
||||
+ raise (Compat.Exc_located(s,FailError (lvl - 1, s')))
|
||||
+ | Compat.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
|
||||
+ raise (Compat.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s'))))
|
||||
|
||||
(* Interprets the clauses of a recursive LetIn *)
|
||||
and interp_letrec ist gl llc u =
|
||||
Index: ide/coq.ml
|
||||
===================================================================
|
||||
--- ide/coq.ml (revision 15024)
|
||||
+++ ide/coq.ml (revision 15025)
|
||||
@@ -112,7 +112,7 @@
|
||||
| _ -> true
|
||||
|
||||
let user_error_loc l s =
|
||||
- raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s)))
|
||||
+ raise (Compat.Exc_located (l, Util.UserError ("CoqIde", s)))
|
||||
|
||||
type printing_state = {
|
||||
mutable printing_implicit : bool;
|
||||
@@ -443,7 +443,7 @@
|
||||
let rec is_pervasive_exn = function
|
||||
| Out_of_memory | Stack_overflow | Sys.Break -> true
|
||||
| Error_in_file (_,_,e) -> is_pervasive_exn e
|
||||
- | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
|
||||
+ | Compat.Exc_located (_,e) -> is_pervasive_exn e
|
||||
| DuringCommandInterp (_,e) -> is_pervasive_exn e
|
||||
| _ -> false
|
||||
|
||||
@@ -456,7 +456,7 @@
|
||||
in
|
||||
let (loc,exc) =
|
||||
match exc with
|
||||
- | Stdpp.Exc_located (loc, ie) -> (Some loc),ie
|
||||
+ | Compat.Exc_located (loc, ie) -> (Some loc),ie
|
||||
| Error_in_file (s, (_,fname, loc), ie) -> None, ie
|
||||
| _ -> dloc,exc
|
||||
in
|
||||
Index: parsing/ppvernac.ml
|
||||
===================================================================
|
||||
--- parsing/ppvernac.ml (revision 15024)
|
||||
+++ parsing/ppvernac.ml (revision 15025)
|
||||
@@ -781,7 +781,7 @@
|
||||
(if i = 1 then mt() else int i ++ str ": ") ++
|
||||
pr_raw_tactic tac
|
||||
++ (try if deftac & Pfedit.get_end_tac() <> None then str ".." else mt ()
|
||||
- with UserError _|Stdpp.Exc_located _ -> mt())
|
||||
+ with UserError _|Compat.Exc_located _ -> mt())
|
||||
|
||||
| VernacSolveExistential (i,c) ->
|
||||
str"Existential " ++ int i ++ pr_lconstrarg c
|
||||
Index: proofs/refiner.ml
|
||||
===================================================================
|
||||
--- proofs/refiner.ml (revision 15024)
|
||||
+++ proofs/refiner.ml (revision 15025)
|
||||
@@ -494,15 +494,15 @@
|
||||
let catch_failerror e =
|
||||
if catchable_exception e then check_for_interrupt ()
|
||||
else match e with
|
||||
- | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))
|
||||
- | Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_))) ->
|
||||
+ | FailError (0,_) | Compat.Exc_located(_, FailError (0,_))
|
||||
+ | Compat.Exc_located(_, LtacLocated (_,FailError (0,_))) ->
|
||||
check_for_interrupt ()
|
||||
| FailError (lvl,s) -> raise (FailError (lvl - 1, s))
|
||||
- | Stdpp.Exc_located(s,FailError (lvl,s')) ->
|
||||
- raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
|
||||
- | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
|
||||
+ | Compat.Exc_located(s,FailError (lvl,s')) ->
|
||||
+ raise (Compat.Exc_located(s,FailError (lvl - 1, s')))
|
||||
+ | Compat.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
|
||||
raise
|
||||
- (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s'))))
|
||||
+ (Compat.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s'))))
|
||||
| e -> raise e
|
||||
|
||||
(* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
|
||||
Index: proofs/logic.ml
|
||||
===================================================================
|
||||
--- proofs/logic.ml (revision 15024)
|
||||
+++ proofs/logic.ml (revision 15025)
|
||||
@@ -48,7 +48,7 @@
|
||||
open Pretype_errors
|
||||
|
||||
let rec catchable_exception = function
|
||||
- | Stdpp.Exc_located(_,e) -> catchable_exception e
|
||||
+ | Compat.Exc_located(_,e) -> catchable_exception e
|
||||
| LtacLocated(_,e) -> catchable_exception e
|
||||
| Util.UserError _ | TypeError _
|
||||
| RefinerError _ | Indrec.RecursionSchemeError _
|
||||
1716
math/coq/pkg-plist
1716
math/coq/pkg-plist
File diff suppressed because it is too large
Load diff
Loading…
Add table
Reference in a new issue