From ce34c0a91eb0e3e90270f820967081247a4ef012 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 23 Aug 2004 08:29:37 +0000 Subject: Patched for OCaml 3.08.1 + other minor things. --- debian/TODO | 6 +++++ debian/changelog | 4 ++- debian/control | 2 +- debian/coqide.menu | 4 +++ debian/patches/00list | 1 + debian/patches/ocaml_3.08.1.dpatch | 55 ++++++++++++++++++++++++++++++++++++++ debian/rules | 8 +++--- 7 files changed, 74 insertions(+), 6 deletions(-) create mode 100644 debian/TODO create mode 100644 debian/coqide.menu create mode 100644 debian/patches/00list create mode 100755 debian/patches/ocaml_3.08.1.dpatch diff --git a/debian/TODO b/debian/TODO new file mode 100644 index 00000000..783c4ca5 --- /dev/null +++ b/debian/TODO @@ -0,0 +1,6 @@ +* See if the -libs are arch-independant (I'm not sure but they should be). If + it's the case change them to Arch: all. + +* Move the coqide stuff from /usr/lib/coq/ide to /usr/share/coqide. The variable + lib_ide should be changed to do that. + diff --git a/debian/changelog b/debian/changelog index c50dac73..87fe0318 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,7 +1,9 @@ coq (8.0pl1-3) unstable; urgency=medium + * Small patch to be able to compile with ocaml 3.08.1. * Added a dependency to ocaml-base-nox when coq is compiled in bytecode. - * Added enhaced manpages. + * Added a menu for coqide. + * Enhanced the manpages. * Enhanced the short descriptions of the packages. -- Samuel Mimram Tue, 17 Aug 2004 20:54:25 +0200 diff --git a/debian/control b/debian/control index 2ca8c21b..3c6157d8 100644 --- a/debian/control +++ b/debian/control @@ -4,7 +4,7 @@ Priority: optional Maintainer: Debian OCaml Maintainers Uploaders: Ralf Treinen , Sven Luther , Jerome Marant , Remi Vanicat , Stefano Zacchiroli , Samuel Mimram Standards-Version: 3.6.1 -Build-Depends: debhelper (>= 4.0.0), ocaml-3.08, ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0) +Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox-3.08, ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0) Package: coq Architecture: any diff --git a/debian/coqide.menu b/debian/coqide.menu new file mode 100644 index 00000000..00dc4139 --- /dev/null +++ b/debian/coqide.menu @@ -0,0 +1,4 @@ +?package(coqide):command="/usr/bin/coqide" \ + icon="/usr/share/pixmaps/coq.xpm" \ + needs="X11" \ + section="Apps/Math" title="CoqIde" diff --git a/debian/patches/00list b/debian/patches/00list new file mode 100644 index 00000000..089b7a7b --- /dev/null +++ b/debian/patches/00list @@ -0,0 +1 @@ +ocaml_3.08.1 diff --git a/debian/patches/ocaml_3.08.1.dpatch b/debian/patches/ocaml_3.08.1.dpatch new file mode 100755 index 00000000..8327a7ae --- /dev/null +++ b/debian/patches/ocaml_3.08.1.dpatch @@ -0,0 +1,55 @@ +#! /bin/sh -e +## ocaml_3.08.1.dpatch by Michel Mauny +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: Add parenthesis to arguments of fun since without parenthesis is not accepted anymore by ocaml. + +if [ $# -lt 1 ]; then + echo "`basename $0`: script expects -patch|-unpatch as argument" >&2 + exit 1 +fi + +[ -f debian/patches/00patch-opts ] && . debian/patches/00patch-opts +patch_opts="${patch_opts:--f --no-backup-if-mismatch} ${2:+-d $2}" + +case "$1" in + -patch) patch -p1 ${patch_opts} < $0;; + -unpatch) patch -R -p1 ${patch_opts} < $0;; + *) + echo "`basename $0`: script expects -patch|-unpatch as argument" >&2 + exit 1;; +esac + +exit 0 + +@DPATCH@ +diff -urNad /home/smimram/work/gnu/pkg-ocaml-maint/coq/trunk/coq-8.0pl1/contrib/funind/tacinv.ml4 coq-8.0pl1/contrib/funind/tacinv.ml4 +--- /home/smimram/work/gnu/pkg-ocaml-maint/coq/trunk/coq-8.0pl1/contrib/funind/tacinv.ml4 2004-02-10 17:22:14.000000000 +0100 ++++ coq-8.0pl1/contrib/funind/tacinv.ml4 2004-08-20 14:40:56.000000000 +0200 +@@ -495,7 +495,7 @@ + let metav = mknewmeta() in + let substmeta t = popn 1 (substitterm 0 (mkRel 1) metav t) in + let newrec_call = substmeta rec_call in +- let newlevar = List.map (fun ev,tev -> ev, substmeta tev) levar in ++ let newlevar = List.map (fun (ev,tev) -> ev, substmeta tev) levar in + let newabsc = Array.map substmeta absc in + newrec_call,newlevar,lposeq,evararr,newabsc,((metav,nme, typ)::parms) + +@@ -693,7 +693,7 @@ + (* Generalize the goal. [[x1:T1][x2:T2]... g[arg1 <- x1 ...]]. *) + let gl_abstr' = add_lambdas (pf_concl gl) gl listargs' in + (* apply parameters immediately *) +- let gl_abstr = applistc gl_abstr' (List.map (fun x,y,z -> x) (List.rev parms)) in ++ let gl_abstr = applistc gl_abstr' (List.map (fun (x,y,z) -> x) (List.rev parms)) in + + (* we apply args of the fix now, the parameters will be applied later *) + let princ_proof_applied_args = +@@ -790,7 +790,7 @@ + in + let rec princ_replace_params params t = + List.fold_left ( +- fun acc ev,nam,typ -> ++ fun acc (ev,nam,typ) -> + mkLambda (Name (id_of_name nam) , typ, + substitterm 0 ev (mkRel 1) (lift 0 acc))) + t (List.rev params) in diff --git a/debian/rules b/debian/rules index 9f88bf6d..b48761d8 100755 --- a/debian/rules +++ b/debian/rules @@ -1,6 +1,8 @@ #!/usr/bin/make -f # debian/rules for coq +include /usr/share/dpatch/dpatch.make + COQPREF=$(CURDIR)/debian/tmp ADDPREF=COQINSTALLPREFIX=$(COQPREF) @@ -18,10 +20,9 @@ configure-stamp: fi touch configure-stamp -build: configure-stamp build-stamp +build: patch-stamp configure-stamp build-stamp build-stamp: dh_testdir - touch test-suite/success/debian.v8 if grep -q BEST=opt config/Makefile; \ then \ ($(MAKE) check \ @@ -38,7 +39,7 @@ build-stamp: fi touch build-stamp -clean: +clean: unpatch dh_testdir dh_testroot rm -f build-stamp configure-stamp opt-stamp @@ -72,7 +73,6 @@ install: build dh_install --sourcedir=$(COQPREF) - #TODO: change lib_ide to /usr/share/coqide cp ide/index_urls.txt debian/coqide/usr/lib/coq/ide/index_urls.txt if [ -e opt-stamp ]; then \ cp debian/coq/usr/share/man/man1/coq-interface.1 debian/coq/usr/share/man/man1/coq-interface.opt.1; \ -- cgit v1.2.3