The following commit has been merged in the master branch: commit 3f1cf9c3ac487d1bf39a8612e1bac997594651b1 Author: Hendrik Tews <hend...@askra.de> Date: Fri Mar 16 10:34:17 2012 +0100
initial packaging diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..337c126 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +*~ +.pc \ No newline at end of file diff --git a/debian/README.Debian b/debian/README.Debian new file mode 100644 index 0000000..b470895 --- /dev/null +++ b/debian/README.Debian @@ -0,0 +1,12 @@ +HOL Light for Debian +-------------------- + +For information on how to use HOL Light, please visit the HOL Light +website at http://www.cl.cam.ac.uk/~jrh13/hol-light/ + +HOL Light runs inside an OCaml toplevel. On every session start, the +logical core and all auxilary theorems are loaded as sources into the +OCaml toplevel. On modern hardware this takes about 2 minutes. + + + -- Hendrik Tews <hend...@askra.de>, Thu, 15 Mar 2012 16:29:01 +0100 diff --git a/debian/changelog b/debian/changelog new file mode 100644 index 0000000..2b7d72d --- /dev/null +++ b/debian/changelog @@ -0,0 +1,5 @@ +hol-light (20120312-1) unstable; urgency=low + + * Initial release (Closes: #663754) + + -- Hendrik Tews <hend...@askra.de> Fri, 16 Mar 2012 10:24:24 +0100 diff --git a/debian/compat b/debian/compat new file mode 100644 index 0000000..ec63514 --- /dev/null +++ b/debian/compat @@ -0,0 +1 @@ +9 diff --git a/debian/control b/debian/control new file mode 100644 index 0000000..239a055 --- /dev/null +++ b/debian/control @@ -0,0 +1,32 @@ +Source: hol-light +Section: math +Priority: optional +Maintainer: Debian OCaml Maintainers <debian-ocaml-ma...@lists.debian.org> +Uploaders: + Hendrik Tews <hend...@askra.de> +Build-Depends: + camlp5 (>= 6.0.4), + ocaml-base-nox, + dh-ocaml (>= 0.9~), + debhelper (>= 9.0.0) +Standards-Version: 3.9.3 +Homepage: http://www.cl.cam.ac.uk/~jrh13/hol-light/ +Vcs-Git: git://git.debian.org/git/pkg-ocaml-maint/packages/hol-light.git +Vcs-Browser: http://git.debian.org/?p=pkg-ocaml-maint/packages/hol-light.git + +Package: hol-light +Architecture: all +Depends: + camlp5, + ocaml-base-nox-${F:OCamlABI}, + ${ocaml:Depends}, + ${shlibs:Depends}, + ${misc:Depends} +Suggests: + readline-editor +Description: HOL Light theorem prover + HOL Light is an interactive theorem prover for Higher-Order Logic + with a very simple logical core running in an OCaml toplevel. HOL + Light is famous for the verification of floating-point + arithmetic as well as for the Flyspec project, which aims at the + formalization of Tom Hales' proof of the Kepler conjecture. diff --git a/debian/copyright b/debian/copyright new file mode 100644 index 0000000..da14a0b --- /dev/null +++ b/debian/copyright @@ -0,0 +1,58 @@ +Format: http://dep.debian.net/deps/dep5 +Upstream-Name: hol-light +Upstream-Contact: John Harrison <jo...@ichips.intel.com> +Source: svn repository at http://hol-light.googlecode.com/svn/trunk + +Files: * +Copyright: 1998 University of Cambridge + 1998-2012 John Harrison <jo...@ichips.intel.com> +License: HOL Light + HOL Light, hereinafter referred to as "the software", is a + computer theorem proving system written by John Harrison. Much of the + software was developed at the University of Cambridge Computer Laboratory, + New Museums Site, Pembroke Street, Cambridge, CB2 3QG, England. The + software is copyright, University of Cambridge 1998 and John Harrison + 1998-2007. + . + Permission to use, copy, modify, and distribute the software and its + documentation for any purpose and without fee is hereby granted. In the + case of further distribution of the software the present text, including + copyright notice, licence and disclaimer of warranty, must be included in + full and unmodified form in any release. Distribution of derivative + software obtained by modifying the software, or incorporating it into + other software, is permitted, provided the inclusion of the software is + acknowledged and that any changes made to the software are clearly + documented. + . + John Harrison and the University of Cambridge disclaim all warranties + with regard to the software, including all implied warranties of + merchantability and fitness. In no event shall John Harrison or the + University of Cambridge be liable for any special, indirect, + incidental or consequential damages or any damages whatsoever, + including, but not limited to, those arising from computer failure or + malfunction, work stoppage, loss of profit or loss of contracts. + + +Files: debian/* +Copyright: 2012 Hendrik Tews <hend...@askra.de> +License: GPL-2+ + This program is free software; you can redistribute it + and/or modify it under the terms of the GNU General Public + License as published by the Free Software Foundation; either + version 2 of the License, or (at your option) any later + version. + . + This program is distributed in the hope that it will be + useful, but WITHOUT ANY WARRANTY; without even the implied + warranty of MERCHANTABILITY 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 along with this package; if not, write to the Free + Software Foundation, Inc., 51 Franklin St, Fifth Floor, + Boston, MA 02110-1301 USA + . + On Debian systems, the full text of the GNU General Public + License version 2 can be found in the file + `/usr/share/common-licenses/GPL-2'. diff --git a/debian/docs b/debian/docs new file mode 100644 index 0000000..7310bfc --- /dev/null +++ b/debian/docs @@ -0,0 +1,3 @@ +QUICK_REFERENCE.txt +README +VERYQUICK_REFERENCE.txt diff --git a/debian/hol-light-source.exclude b/debian/hol-light-source.exclude new file mode 100644 index 0000000..448c8ea --- /dev/null +++ b/debian/hol-light-source.exclude @@ -0,0 +1,11 @@ +./debian +./.git +./.gitignore +./CHANGES +./LICENSE +./Makefile +./pa_j*.ml +./QUICK_REFERENCE.txt +./README +./VERYQUICK_REFERENCE.txt +./holtest diff --git a/debian/hol-light.1 b/debian/hol-light.1 new file mode 100644 index 0000000..e829ec9 --- /dev/null +++ b/debian/hol-light.1 @@ -0,0 +1,58 @@ +.\" Hey, EMACS: -*- nroff -*- +.\" First parameter, NAME, should be all caps +.\" Second parameter, SECTION, should be 1-8, maybe w/ subsection +.\" other parameters are allowed: see man(7), man(1) +.TH HOL-LIGHT 1 "March 16, 2012" +.\" Please adjust this date whenever revising the manpage. +.\" +.\" Some roff macros, for reference: +.\" .nh disable hyphenation +.\" .hy enable hyphenation +.\" .ad l left justify +.\" .ad b justify to both left and right margins +.\" .nf disable filling +.\" .fi enable filling +.\" .br insert line break +.\" .sp <n> insert n+1 empty lines +.\" for manpage-specific macros, see man(7) +.SH NAME +hol-light \- HOL Light interactive theorem prover +.SH SYNOPSIS +.B hol-light +.RI "[options...]" +.SH DESCRIPTION +The command +.B hol-light +is a simple wrapper for calling +.B ocaml +and loading the HOL Light basic definitions (by loading +.I /usr/share/hol-light/hol.ml +instead of +.B .ocamlinit +as initialization file). Loading these definitions takes about 2 +minutes on modern hardware, please be patient. All options and +other arguments are passed as options to +.B ocaml\fR. +.\"========================================================================== +.P +If you have a +.B readline-editor +such as +.B rlwrap\fR, \fBledit\fR or \fBrlfe +installed, the +.B hol-light ocaml +toplevel is wrapped in +.B readline-editor\fR. +Install just one of these readline editors or configure your +preferred one via the alternative system. +.SH SEE ALSO +.BR ocaml "(1), " readline-editor "(1), " rlwrap "(1), " ledit "(1), " rlfe (1) +.br +HOL Light documentation at +.I http://www.cl.cam.ac.uk/~jrh13/hol-light/ +.SH AUTHOR +The +.B hol-light +script and this manual page were written +by Hendrik Tews <hend...@askra.de>, +specifically for the Debian project (and may be used by others). diff --git a/debian/hol-light.manpages b/debian/hol-light.manpages new file mode 100644 index 0000000..16dab92 --- /dev/null +++ b/debian/hol-light.manpages @@ -0,0 +1 @@ +debian/hol-light.1 \ No newline at end of file diff --git a/debian/hol-light.sh b/debian/hol-light.sh new file mode 100755 index 0000000..a467605 --- /dev/null +++ b/debian/hol-light.sh @@ -0,0 +1,11 @@ +#!/bin/sh + +#set -xe + +if [ -f /usr/bin/readline-edito ] ; then + readline=/usr/bin/readline-editor +else + readline= +fi + +$readline /usr/bin/ocaml $* -init /usr/share/hol-light/hol.ml diff --git a/debian/menu b/debian/menu new file mode 100644 index 0000000..e3d55f2 --- /dev/null +++ b/debian/menu @@ -0,0 +1,2 @@ +?package(hol-light):needs="text" section="Applications/Science/Mathematics"\ + title="HOL Light" command="/usr/bin/hol-light" diff --git a/debian/patches/default-hollight-dir b/debian/patches/default-hollight-dir new file mode 100644 index 0000000..4acdbd3 --- /dev/null +++ b/debian/patches/default-hollight-dir @@ -0,0 +1,22 @@ +Description: configure default HOL Light source directory +Author: Hendrik Tews <hend...@askra.de> +--- a/hol.ml ++++ b/hol.ml +@@ -11,8 +11,16 @@ + + let hol_version = "2.20++";; + ++let debian_hol_light_dir = "/usr/share/hol-light" ++ + let hol_dir = ref +- (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());; ++ (try Sys.getenv "HOLLIGHT_DIR" ++ with Not_found -> ++ try ++ if Sys.is_directory debian_hol_light_dir ++ then debian_hol_light_dir ++ else raise (Sys_error "") ++ with Sys_error _ -> Sys.getcwd());; + + (* ------------------------------------------------------------------------- *) + (* Should eventually change to "ref(Filename.temp_dir_name)". *) diff --git a/debian/patches/series b/debian/patches/series new file mode 100644 index 0000000..c914661 --- /dev/null +++ b/debian/patches/series @@ -0,0 +1 @@ +default-hollight-dir diff --git a/debian/rules b/debian/rules new file mode 100755 index 0000000..6e81989 --- /dev/null +++ b/debian/rules @@ -0,0 +1,47 @@ +#!/usr/bin/make -f +# -*- makefile -*- +# Sample debian/rules that uses debhelper. +# +# This file was originally written by Joey Hess and Craig Small. +# As a special exception, when this file is copied by dh-make into a +# dh-make output file, you may use that output file without restriction. +# This special exception was added by Craig Small in version 0.37 of dh-make. +# +# Modified to make a template file for a multi-binary package with separated +# build-arch and build-indep targets by Bill Allombert 2001 + +# Uncomment this to turn on verbose mode. +export DH_VERBOSE=1 +export DH_OPTIONS=-v + +include /usr/share/ocaml/ocamlvars.mk + +CAMLP5_ABI ?= $(shell /usr/bin/camlp5 -v 2>&1 | { read a b c d && echo $$c; }) + +# This has to be exported to make some magic below work. +export DH_OPTIONS + + +%: + dh $@ + +.PHONY: override_dh_auto_build +override_dh_auto_build: + cp pa_j_3.1x_6.02.2.ml pa_j.ml + make + +INSTDIR:=debian/hol-light +.PHONY: override_dh_auto_install +override_dh_auto_install: + install -d $(INSTDIR)/usr/share/hol-light + tar --anchored --exclude-from=debian/hol-light-source.exclude -c . | \ + tar -C $(INSTDIR)/usr/share/hol-light -x + chmod 644 $(INSTDIR)/usr/share/hol-light/Unity/README + chmod 644 $(INSTDIR)/usr/share/hol-light/100/e_is_transcendental.ml + install -d $(INSTDIR)/usr/bin + install debian/hol-light.sh $(INSTDIR)/usr/bin/hol-light + +.PHONY: override_dh_gencontrol +override_dh_gencontrol: + dh_gencontrol -- -VF:OCamlABI="$(OCAML_ABI)" \ + -VF:Camlp5ABI="$(CAMLP5_ABI)" diff --git a/debian/source/format b/debian/source/format new file mode 100644 index 0000000..163aaf8 --- /dev/null +++ b/debian/source/format @@ -0,0 +1 @@ +3.0 (quilt) diff --git a/debian/watch b/debian/watch new file mode 100644 index 0000000..fb7467b --- /dev/null +++ b/debian/watch @@ -0,0 +1,8 @@ +# format version number, currently 3; this line is compulsory! +version=3 + +# The upstream version of HOL Light is only available as svn repository +# at http://hol-light.googlecode.com/svn/trunk . There are no releases. +# +# If there is a way to let uscan check svn revision numbers then please +# tell me! diff --git a/hol.ml b/hol.ml index 843b11f..c19c860 100644 --- a/hol.ml +++ b/hol.ml @@ -11,8 +11,16 @@ let hol_version = "2.20++";; +let debian_hol_light_dir = "/usr/share/hol-light" + let hol_dir = ref - (try Sys.getenv "HOLLIGHT_DIR" with Not_found -> Sys.getcwd());; + (try Sys.getenv "HOLLIGHT_DIR" + with Not_found -> + try + if Sys.is_directory debian_hol_light_dir + then debian_hol_light_dir + else raise (Sys_error "") + with Sys_error _ -> Sys.getcwd());; (* ------------------------------------------------------------------------- *) (* Should eventually change to "ref(Filename.temp_dir_name)". *) -- hol-light packaging _______________________________________________ Pkg-ocaml-maint-commits mailing list Pkg-ocaml-maint-commits@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits