cjex / hol-light Goto Github PK
View Code? Open in Web Editor NEWHOL Light is an interactive theorem prover / proof checker. Automatically exported from code.google.com/p/hol-light
License: Other
HOL Light is an interactive theorem prover / proof checker. Automatically exported from code.google.com/p/hol-light
License: Other
What steps will reproduce the problem?
1. load ocaml and hol.ml as usual
2. loadt "Library/analysis.ml";;
3. loadt "Multivariate/vectors.ml";;
What is the expected output? What do you see instead?
Expecting exit with no problems. Instead, it exits with the final lines:
val DOT_RMUL : thm = |- !c x y. x dot c % y = c * (x dot y)
Warning: inventing type variables
Exception: Failure "GEN_TAC".
Error in included file
/home/ivan/Dropbox/ReadSterling/hol_light/Multivariate/vectors.ml
val it : unit = ()
What version of the product are you using? On what operating system?
2.20++ , Linux Mint
Please provide any additional information below.
It appears that the "--" defined in analysis.ml conflicts somehow with the "--"
defined in realax.ml , or I may be completely off.
Original issue reported on code.google.com by [email protected]
on 2 Mar 2014 at 10:52
Reference manual of REWRITE_CONV points to undocumented SUBST_CONV.
Original issue reported on code.google.com by [email protected]
on 24 Jul 2014 at 1:27
The attached patch fixes a minor issue in two help descriptions.
Original issue reported on code.google.com by [email protected]
on 16 Aug 2014 at 8:15
Attachments:
Several code examples in documentation contain extra space after "#" char.
Patch attached.
Original issue reported on code.google.com by [email protected]
on 23 Jul 2014 at 8:49
Attachments:
The attached patch documents failure conditions of 'is_hidden'.
Original issue reported on code.google.com by [email protected]
on 24 Jul 2014 at 8:24
Attachments:
In few places in the documentation "i.e." is followed by extra comma (,).
Attached patch makes the punctuation consistent with "e.g." and other uses
"i.e.".
Original issue reported on code.google.com by [email protected]
on 23 Jul 2014 at 8:13
Attachments:
Documentation for GEN_REWRITE_TAC seems to be copied from HOL4, but in HOL
Light this tactic takes only two arguments, not three. Patch attached.
Original issue reported on code.google.com by [email protected]
on 7 Sep 2014 at 10:26
Attachments:
I installed OCaml 4.00.0 and camlp5 using GODI a while back. Today, I checked
out the hol-light sources, but when I tried building them I got the following
error:
File "pa_j.ml", line 13, characters 0-10:
Error: Unbound module Pcaml
make: *** [pa_j.cmo] Error 2
After a bit of searching, I found that ocamlc treats the `-I +foo` argument as
`-I /usr/lib/ocaml/foo`:
http://stackoverflow.com/questions/3848897/unbound-modules-in-ocaml
As it turns out, GODI installs camlp5 in a non-standard location. On this
machine (Ubuntu 12.04.1 x86), `which camlp5` returns:
/opt/godi/bin/camlp5
So, I tweaked the Makefile a bit to make it more robust (see the attached
diff). camlp4 and camlp5 both support the "-where" option, so I've used that
within backticks along with the -I option when invoking ocamlc. This makes it
so camlp4/camlp5 will be included properly no matter where it's installed on
the system.
Cheers,
Jack
Original issue reported on code.google.com by [email protected]
on 14 Feb 2013 at 9:22
Attachments:
pa_j.ml: parse error after upgrade to ocaml 3.12 and camlp5 6.02
kx@linux:~/tmp/hol_light_svn> make
if test `ocamlc -version | cut -c3` = "0" ; \
then ocamlc -c -pp "camlp4r pa_extend.cmo q_MLast.cmo" -I +camlp4 pa_j.ml; \
else ocamlc -c -pp "camlp5r pa_lexer.cmo pa_extend.cmo q_MLast.cmo" -I +camlp5 pa_j.ml; \
fi
File "pa_j.ml", line 1689, characters 37-56:
While expanding quotation "class_expr":
Parse error: ']' or [expr] expected after '[' (in [expr])
File "pa_j.ml", line 1, characters 0-1:
Error: Preprocessor error
make: *** [pa_j.cmo] Error 2
Original issue reported on code.google.com by [email protected]
on 16 Nov 2010 at 11:00
This causes user pretty-printers to print directly to the console, instead of
the correct destination known to the formatter (e.g., a target string in
string_of_term).
I attach a patchfile that fixes this that can be applied using the command
patch -p0 < patchfile
Note: it changes the type of user pretty-printers by adding the formatter as an
argument, so existing user pretty-printers will need to be updated.
Original issue reported on code.google.com by [email protected]
on 3 Mar 2014 at 12:31
Attachments:
What steps will reproduce the problem?
1. Install OCaml 3.12.0 on Mac OS X 10.5.8 from prebuilt binaries
2. Download camlp5-6.02.2, apply two patches, and build.
3. Check out most recent verson of HOL Light with svn, and do make.
What is the expected output? What do you see instead?
I get this error message from make:
File "pa_j.ml", line 195, characters 6-21:
Error: The constructor PaLab expects 2 argument(s),
but is applied here to 3 argument(s)
make: *** [pa_j.cmo] Error 2
What version of the product are you using? On what operating system?
Revision 83 on Mac OS 10.5.8.
Please provide any additional information below.
Can you tell me a combination of a version of HOL Light and a version of camlp5
that work together? I had other problems when I tried building the 10 Jan 2010
snapshot you have on the HOL Light home page.
Original issue reported on code.google.com by [email protected]
on 19 Mar 2011 at 3:19
Documentation of new_type's FAILURE CONDITIONS contains a grammar error (or a
grammar mistake): "Fails if HOL is there is already a type operator..."
Original issue reported on code.google.com by [email protected]
on 23 Jul 2014 at 7:54
What steps will reproduce the problem?
1. svn checkout
2. make
3.
What is the expected output? What do you see instead?
File "pa_j.ml", line 195, characters 6-21:
Error: The constructor PaLab expects 2 argument(s),
but is applied here to 3 argument(s)
What version of the product are you using? On what operating system?
camlp5 6.06
Please provide any additional information below.
This patch seems to solve the problem
Index: Makefile
===================================================================
--- Makefile (revision 146)
+++ Makefile (working copy)
@@ -56,7 +56,7 @@
then cp pa_j_${OCAML_VERSION}.ml pa_j.ml ; \
else if test ${CAMLP5_VERSION} = "6.02.1" ; \
then cp pa_j_3.1x_6.02.1.ml pa_j.ml; \
- else if test ${CAMLP5_VERSION} = "6.02.2" -o ${CAMLP5_VERSION} =
"6.02.3" -o ${CAMLP5_VERSION} = "6.05" ; \
+ else if test ${CAMLP5_VERSION} = "6.02.2" -o ${CAMLP5_VERSION} =
"6.02.3" -o ${CAMLP5_VERSION} = "6.05" -o ${CAMLP5_VERSION} = "6.06" ; \
then cp pa_j_3.1x_6.02.2.ml pa_j.ml; \
else cp pa_j_3.1x_${CAMLP5_BINARY_VERSION}.xx.ml pa_j.ml; \
fi \
Original issue reported on code.google.com by [email protected]
on 20 Aug 2012 at 4:42
Patch attached.
Original issue reported on code.google.com by [email protected]
on 7 Sep 2014 at 8:48
Attachments:
Here's a patch to the print_to_string function that accesses the current line
length using a call to get_margin before printing the argument to a string. I
also recoded the print_to_string function in terms of ocaml buffers, instead of
a string reference.
The patchfile can be applied using the command
patch -p0 < patchfile
Original issue reported on code.google.com by [email protected]
on 3 Mar 2014 at 12:37
Attachments:
What steps will reproduce the problem?
1. Install the Windows version of OCaml
2. Download Camlp5 and apply all 3 patches, "configure", "make" and "make
install"
3. Download the HOL Light source and try to "make" it
What is the expected output? What do you see instead?
File "pa_j.ml", line 112, characters 72-74:
Error: This expression has type (string * MLast.ctyp) list
but is here used with type ('a * MLast.ctyp) list Ploc.vala
make: *** [pa_j.cmo] Error 2
What version of the product are you using? On what operating system?
Windows 7 Professional
OCaml: 3.11.0, MinGW port
Camlp5: 6.02.2-3
HOL Light: revision 86
MSys to run patch, make etc.
Please provide any additional information below.
Original issue reported on code.google.com by [email protected]
on 2 Apr 2011 at 4:31
There are three semicolons instead of two in the documentation of SPECL (typo).
Patch attached.
Original issue reported on code.google.com by [email protected]
on 30 Jul 2014 at 10:08
Attachments:
Its presence here https://github.com/jbem/dead-souls suggests that the project
is abandoned. The link on the hol-light home page (and google code page) is
broken.
Original issue reported on code.google.com by [email protected]
on 4 Sep 2011 at 10:31
I checked out from the subversion repository (r146) and executed make in the
root directory and got the error message above returned. A quick look at the
directory showed that it is really not there:
[user@hostname hol-light-read-only]$ ls -1 pa_j*
pa_j_3.07.ml
pa_j_3.08.ml
pa_j_3.09.ml
pa_j_3.1x_5.xx.ml
pa_j_3.1x_6.02.1.ml
pa_j_3.1x_6.02.2.ml
pa_j_3.1x_6.xx.ml
as far as i could see, these files are not automatically generated - is it
possible that they are only missing in the repository or am I doing something
wrong? Thanks in advance, Martin
Original issue reported on code.google.com by [email protected]
on 29 Aug 2012 at 2:12
Chapter 11 (Page 74, file 'tutorial_220.pdf'); is "far from a a simple", should
be "far from a simple".
Original issue reported on code.google.com by [email protected]
on 29 Jul 2014 at 10:24
What steps will reproduce the problem?
1. svn checkout http://hol-light.googlecode.com/svn/trunk/ hol-light-read-only
2. make
3.
What is the expected output? What do you see instead?
I get the error message:
File "pa_j.ml", line 1918, characters 35-43:
While expanding quotation "str_item":
Parse error: antiquot "_" or antiquot "" or [ident] expected after 'type' (in
[str_item])
File "pa_j.ml", line 1:
Error: Preprocessor error
make: *** [pa_j.cmo] Error 2
What version of the product are you using? On what operating system?
OCaml 4.00.1
Linux Fedora 18
Please provide any additional information below.
I am trying to build HOL Light with OCaml 4, but the build bombs out with the
above error message.
Original issue reported on code.google.com by [email protected]
on 27 Oct 2013 at 7:39
What steps will reproduce the problem?
1. Install the Windows version of OCaml
2. Download Camlp5 and apply all 3 patches, "configure", "make" and "make
install"
3. Download the HOL Light source and try to "make" it
What is the expected output? What do you see instead?
File "pa_j.ml", line 112, characters 72-74:
Error: This expression has type (string * MLast.ctyp) list
but is here used with type ('a * MLast.ctyp) list Ploc.vala
make: *** [pa_j.cmo] Error 2
What version of the product are you using? On what operating system?
Windows 7 Professional
OCaml: 3.11.0, MinGW port
Camlp5: 6.02.2-3
HOL Light: revision 86
MSys to run patch, make etc.
Please provide any additional information below.
Original issue reported on code.google.com by [email protected]
on 2 Apr 2011 at 4:31
What steps will reproduce the problem?
Execute these commands:
# needs "Examples/prog.ml";;
# install_parser ("correct",parse_program_assertion);;
# g `correct
T
var x;
x := 1
end
x > 0`;;
# e VC_TAC;;
What is the expected output? What do you see instead?
VC_TAC should generate verification conditions `1 > 0`, but it leaves the goal
unmodified.
What version of the product are you using? On what operating system?
HOL Light from SVN, revision 200; ocaml 4.01.0, Linux
Please provide any additional information below.
VC_TAC works as expected if I introduce a dummy variable:
# g `correct T var x, dummy; x := 1 end x > 0`;;
Original issue reported on code.google.com by [email protected]
on 20 Oct 2014 at 9:50
There are some minor issues with set_goal package documentation, e.g. missing
cross-references and extra space. Patch attached.
Original issue reported on code.google.com by [email protected]
on 24 Jul 2014 at 10:41
Attachments:
What steps will reproduce the problem?
1. Install camlp5-6.12 (released 2014-09-19)
2. Checkout the source of hol-light (revision 199)
3. Run `make`
What is the expected output? What do you see instead?
The compilation fails, because the wrong file was copied to `pa_j.ml`.
What version of the product are you using? On what operating system?
hol-light r199 on linux x86_64 with ocaml 4.01.0 and camlp5 6.12
Please provide any additional information below.
Original issue reported on code.google.com by [email protected]
on 30 Sep 2014 at 11:59
Attachments:
As in the summary.
Original issue reported on code.google.com by [email protected]
on 24 Jul 2014 at 11:29
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.