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
