add comment to mark proofs in vim as foldable

Because vim folds are rather used by advanced vim users, this addition is
a comment.

set vim syntax to latex for pre-munger *.htex files

Provide plausible default (not []) for POLY_LDFLAGS on all platforms

Acknowledge Cygwin without doing anything other than slotting in the
default value for the moment.

Set up Poly/ML configure so that POLY_LDFLAGS can be overridden

In particular, it is now possible to write

val POLY_LDFLAGS = ["-lfoo", ...]

in a tools-poly/poly-includes.ML file and have this override the
system's own choice of value for this. This is also possible for
POLY_LDFLAGS_STATIC.

Update tags to label release as Kananaskis-13

Remove unwarranted claim that emacs mode works for XEmacs

Compatibility with XEmacs hasn't been tested in ages, and as XEmacs
seems to be getting very little development love itself, I don't feel
too bothered by this.

Some heap paths need to be quoted, e.g. those involving a directory called "a - b".

Insist on PolyML version >= 5.7.0 in configure

Older versions don't have RunCall.loadWord, which is used by the
concurrency code in src/portableML/poly

Update release details in configure.sml files

These feed in to what is displayed in the interactive REPL's banner.

Write tool to generate most of a .uo file for a Script.sml file

The output is "the same" as that which is fed to buildheap when a
script file is executed, except that the actual Script.sml file is not
mentioned, allowing some other file to be generated.

Try to find dot in user's PATH during configuration

If it is not found, say little about its absence on help-graph build
time.

Make Poly linking on MacOS use -lstdc++ if pkg-config fails us

Can't just omit -lgmp when Poly has been compiled to expect it

My test that seemed to indicate I could must have been broken, or not
properly performed.

Not including -lgmp seems safest on Linux

Update link options for Linux building of executables

Fix POLY_LDFLAGS (with reference to polyc executable)

Get basic interactive executables to work

Make it possible to stop using MLTON; make it clear if it is used

Use mlton to compile build and Holmake if it is installed

This is based on the theory that it won't generate strange errors on
wait as some versions of Poly/ML still seem prone to. It is probably
also quicker. (The script files themselves are still executing Poly/ML
so it's an improvement at the margins only.)

Make Moscow ML dep. calculation unquote-free as well

This allows yet more pleasant refactoring (with the
FNameToUnquotedDeps module completely disappearing). Now there is a
generally useful QFRead module in tools/Holmake that allows the
quotation machinery to be applied to strings and files.

The quotation filter is still a "push" technology: it consumes
everything it can and outputs as it goes. (It does block if its input
stream blocks of course.) I think it would be nice to modify the
filter (now QuoteFilter in tools/Holmake) so that it was "pull", the
client getting to pull chunks of output a bit at a time.

Currently, the API supports "reader" operations of type unit -> char
option, and these look like pull operations, but these are pulls on a
buffer that has already been filled with as much output as possible.

Complete relocation-build feature

Closes #105

To be explicit, after building HOL in one directory one can then

$ bin/build cleanForReloc
$ cd ..
$ mv HOL somewhere_else
$ cd somewhere_else
$ poly < tools/smart-configure.sml
$ bin/build --relocbuild

The last step (the "relocation" build) takes less than a minute and
results in a functional system that is housed in a different location.

Next step on this branch of work is to provide tools allowing other
developments (those not under HOLDIR) to be moved in a similar way.

Move script that builds Holmake out of tools-poly

Eventually, tools-poly/Holmake should disappear

Ensure HOL4 works with fixed-width integers under Poly/ML.

Integers under Poly/ML 5.6.1 are likely to be fixed-width by default (up until now they've always been arbitrary precision). Some changes were needed to cope with this:

- The Arbint and Artbnum structures effectively assumed Int.int = IntInf.int.
- The Standard ML structure Time is based on LargeInt.int and not Int.int. Code for printing times has been re-implemented using the Date structure.
- The smart-configure.sml file used the Overflow exception to distinguish between Moscow ML and Poly/ML. This test is now based on a difference in the printing of General.Fail exceptions.

POLYC + POLY_VERSION now available in Holmakefiles

Also change POLYC from string option to string in Systeml (and "" in
Moscow ML environments).

Insist on Poly/ML version >= 5.5.1

Add -lgmp flag.

Use PolyML.SaveState instead of executable heaps

Interface in terms of "HOLHEAP" declarations in Holmakefiles stays the
same. Implementation uses hierarchical saved states. All command-line
executables should also now be compiled with polyc.

Closes #292

Adaptations in preparation for the release of Poly/ML 5.6.

Note that HOL4 now relies on PolyML.addPrettyPrinter and PolyML.Compiler.compilerVersionNumber, which came with Poly/ML version 5.3.

Adaptations in preparation for the release of Poly/ML 5.6.

Note that HOL4 now relies on PolyML.addPrettyPrinter and PolyML.Compiler.compilerVersionNumber, which came with Poly/ML version 5.3.

Next release will be Kananaskis-11

This commit starts release preparation branch.

Use polyc for all compilation in configure.sml

I don't think I can use polyc in the creation of a new heap that is done
within buildheap though, which means that I believe we still have to
tell users to build poly with --enable-shared.

Progress with #292

Detect availability of polyc at config time

Work towards issue #292

use /bin/sh instead of /bin/bash (which is not available on all UNIX systems)

also, use cc instead of gcc (no need to compile HOL4 with gcc)

Implement (efficient) holdep lexing by hand.

Without using references (except in the side-effecting stream reading,
I suppose). In any case, performance in Poly/ML is much better (~4s
on my old Mac for holdeptool on the 30MB CakeML theory.sml file).

Includes some test-cases.

Make holdeptool available as part of Poly/ML build.

Also slightly tidy up lex implementation: can use inputN as parameter
to makeLexer rather than inputLine.

runholdep function moves to Holmake_tools (Poly/ML Holmake affected)

In the latter module, it can be used in the Poly/ML implementation.
This is progress with github issue #77

The Poly/ML implementation now fails the regression test in

tools/Holmake/tests/depchain1/dir3

so comment out that test from the build sequence temporarily. I
believe there will be a Holmake failure in machine-code until the
behaviour is properly fixed. I hope selftest 2 will go through
correctly.

Holmake's output also changes slightly because I've been more
consistent about using the built-in 'info' function instead of print.

Change Kananaskis-9 into Kananaskis-10 in the relevant places.

Make copy of portable pointer_eq available in Systeml.

This then allows regexpMatch to be portable too.

make running parallel sessions of Vimhol easier

Thanks to Yong Kiam Tan for the idea.

Handle corrupt Systeml.sig when moving build from Moscow ML to Poly.

This is analogous to what was done in b151b8f0 (Jul 2009), which coped
with building a Moscow ML setup on top of a build that used to be
Poly. There the claim was made that the reverse situation (the one
fixed in this commit) didn't need anything done to it. That was
because poly's Systeml.ui was being generated afresh with every
configure, right up until 331d321e (Jan 2014).

Make polyml HOL build successfully when HOLDIR includes spaces.

Force --gcthreads=1 on poly invocations (in crudest way possible)

Closes #146

When possible, avoid "recompiling" Systeml.sig in poly's configure step.

This now means that it's possible to do a reconfigure (perhaps to pick
up a fresh emacs mode change, or a new Holmake feature), without the
next build necessarily rebuilding everything.

Updated version number in manuals, banners etc.

removed -lgmp flag

Avoid duplicate lib flags in configuration for PolyML 5.5.1 (and above) under Darwin.

It is probably better to simplify things further, i.e. make sure users build PolyML using the option --enable-shared (which is no longer the default). In particular, -lgmp is problematic because not all users will build PolyML with GMP support enabled.

Tweaks following release of Poly/ML 5.5.1.

Allow user to configure location of dot tool for theory graph building.

The default is /usr/bin/dot, because that’s where it is on my Linux machine. If you need it to be somewhere else, create a config-override or poly-includes.ML file, depending on which ML you’re using.

Remove uses of PolyML.Compiler.compilerVersionNumber.

This is not bound in PolyML 5.2. When we decide not to support that
version of the compiler, we can stop fussing. For the moment, I’m
running regressions against that compiler on one of the test-machines.

Avoid linker warning messages on Mac OS for Poly/ML 5.5.

Make Systeml.sig the same in Moscow ML and Poly builds.

This additional uniformity allows me to delete the
tools-poly/Holmake/Systeml.sig file. This then requires a bunch of
changes to compilation of the early tools which have to point at
tools/Holmake/Systeml.sig rather than the version in
tools-poly/Holmake.

This should fix the configuration errors on MoscowML introduced by
0a0988fc.

Improvements to the process of generating a custom heap.

The poly configuration process now creates a buildheap executable in
the hol/bin directory. This provides a smoother way to create a
custom heap that has been preloaded with useful theories and ML code.

Make the leading string before Vimhol commands more easily configurable

You can replace the "h" at the start of all Vimhol commands by some
other string by changing the line in your filetype.vim that loads the
Vimhol script.

Unfortunately, if you are happy using "h" already, you may also have to
change that line to match this commit's new version of filetype.vim,
which now explicitly sets up "h" as a default.

Make the hol executable use a directory's HOLHEAP, if given.

This is achieved with a heapname executable that runs before hol
starts, returning the name of the appropriate heap for the current
directory. This determination is made by looking at the local
Holmakefile, if there isn't one, or if it doesn't specify a HOLHEAP
variable, then the usual bin/hol.builder heap is used.

This also works for the hol.noquote executable (though it's hard to
believe anyone uses this).

Remove muddy-related stuff in poly's configure.sml that was commented out.

Update version numbers now that K7 is out.

Bump version numbers - next release to be 'Kananaskis-7'.

Addition of POLY_LDFLAGS_STATIC variable. This variable is used for static linking whereas the recently added POLY_LDFLAGS triggers dynamic linking.

Store (calculated) Poly/ML linker flags into Systeml.

This allows build to read these flags from Systeml, rather than having to
recalculate them.

Make the configure script generate instances of Vimhol scripts with the right paths.

This is analogous to generating hol-mode.el from hol-mode.src for Emacs. I only
changed the PolyML configure script since Vimhol only works with PolyML at the
moment.

Configure now generates hol.vim and vimhol.sml with the HOLDIR paths hard
coded. Therefore there is no longer any need to set up a $HOLDIR environment
variable. We also generate template files for hol-config.sml and filetype.vim
that can be copied to the user's ~ (or ~/.vim) to allow Vimhol to start
automatically.

I also updated the README, and an inaccurate comment in configure.sml.

Apply bits of Thomas's last Emacs mode update (7597) that are OK.

Revert "Added support for calling Holmake to hol-mode. Moreover, ..."

This undows commit 7597, which (unintentionally) undid changes of mine
in 7498. I will re-apply those parts of 7597 that are not broken in a
follow-up.

Added support for calling Holmake to hol-mode. Moreover, some more key-combinations were added.

Edited the configure.sml and build.sml files of tools-poly to recognize when building HOL using Poly/ML under Mac OS X, and if so, to add the options "-segprot POLY rwx rwx" to all compilations/linkings. If the Poly/ML was built for 32-bits, then in addition the options "-arch i386" are added. These options are necessary on the Macintosh for the newer versions of Poly/ML, from 5.3 onward.

Emacs HOL mode: now has a customisation group. If you do M-x
customize, and then select External/Hol, you will get the standard
emacs interface for changing some bits and pieces. Also add the
ppbackend toggle to the HOL menu. (This HOL menu should really only
appear above relevant buffers, not all the time.)

From now on we're in the Brave New World of Kananaskis 6.

Add some comments to the Poly/ML version of configure.sml so that it's
like the Moscow ML version (specifies which variables need to be
filled in).

Put a variable ML_SYSNAME into the Systeml structure recording what ML
implementation is being used.

More fixes for the poly version - I think this should now let the
emacs mode be used with both.

Put a toggle_quietdec function into the Systeml structure, allowing a
common interface to be relied on by the emacs mode.

Modify configuration to use PATH examination to find the poly
executable, and to allow the configuration to be done from the root
hol directory, and not just tools-poly.

Modify poly configuration so that it builds the quotation filter out
of the tools/quote-filter directory. This allows deletion of the copy
of quote-filter in tools-poly.

Trivial changes.

Remove need for poly-tools to have its own mlyacc directory.

Remove need for separate tools-poly/mllex directory.
Also change user configuration experience slightly; put your poly
paths into a file called tools-poly/poly-includes.ML. In the form
val poly = "<path to poly executable>"
val polymllibdir = "<path to directory containing poly's lib files>"
This way we get to avoid changing tools-poly/configure.sml just to get
our own builds working.

Improve the building process under Poly/ML.

A little more polish on the PolyML build.

Streamline the PolyML compatibility support a bit.

Misc fixes to Poly ML compatibility.

PolyML compatibility. See tools-poly/README.