#
8406264f |
|
25-Oct-2018 |
Anthony Fox <anthony.fox@cantab.net> |
Some heap paths need to be quoted, e.g. those involving a directory called "a - b".
|
#
ee54b084 |
|
04-Sep-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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
|
#
baa76973 |
|
17-Jun-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update release details in configure.sml files These feed in to what is displayed in the interactive REPL's banner.
|
#
2338fc68 |
|
06-Feb-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|
#
5dcc0ad1 |
|
10-Dec-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|
#
5ea71409 |
|
16-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make Poly linking on MacOS use -lstdc++ if pkg-config fails us
|
#
330a7b25 |
|
13-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|
#
7468c54b |
|
13-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Not including -lgmp seems safest on Linux
|
#
32b5ebae |
|
12-Sep-2017 |
Michael Norrish <michael.norrish@nicta.com.au> |
Update link options for Linux building of executables
|
#
2d5a1df9 |
|
11-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix POLY_LDFLAGS (with reference to polyc executable)
|
#
d8c2a41b |
|
07-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get basic interactive executables to work
|
#
5d69d290 |
|
23-Jul-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make it possible to stop using MLTON; make it clear if it is used
|
#
c13df663 |
|
20-Jul-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.)
|
#
99c47651 |
|
04-Jun-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|
#
c2615dd8 |
|
18-Apr-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|
#
0a81729c |
|
12-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Move script that builds Holmake out of tools-poly Eventually, tools-poly/Holmake should disappear
|
#
c554f74b |
|
15-Feb-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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.
|
#
a670538a |
|
07-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
POLYC + POLY_VERSION now available in Holmakefiles Also change POLYC from string option to string in Systeml (and "" in Moscow ML environments).
|
#
8901d290 |
|
07-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Insist on Poly/ML version >= 5.5.1
|
#
3a93303b |
|
07-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Add -lgmp flag.
|
#
bded7b18 |
|
07-Jan-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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
|
#
66eaae4d |
|
06-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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.
|
#
ca2ec398 |
|
06-Jan-2016 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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.
|
#
f9053c22 |
|
08-Oct-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Next release will be Kananaskis-11 This commit starts release preparation branch.
|
#
d95e7fd1 |
|
22-Sep-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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
|
#
0c595d32 |
|
22-Sep-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Detect availability of polyc at config time Work towards issue #292
|
#
103c7011 |
|
23-Apr-2015 |
Hannes Mehnert <hannes@mehnert.org> |
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)
|
#
37d61e33 |
|
06-Feb-2015 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|
#
6970522c |
|
03-Feb-2015 |
Michael Norrish <michael.norrish@nicta.com.au> |
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.
|
#
4522c28a |
|
02-Feb-2015 |
Michael Norrish <michael.norrish@nicta.com.au> |
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.
|
#
742e0d6a |
|
05-Nov-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Change Kananaskis-9 into Kananaskis-10 in the relevant places.
|
#
2129ae09 |
|
26-Oct-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Make copy of portable pointer_eq available in Systeml. This then allows regexpMatch to be portable too.
|
#
6fbab843 |
|
23-Aug-2014 |
Ramana Kumar <ramana@member.fsf.org> |
make running parallel sessions of Vimhol easier Thanks to Yong Kiam Tan for the idea.
|
#
5acc4178 |
|
03-Aug-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
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).
|
#
fb5e3bf4 |
|
27-May-2014 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make polyml HOL build successfully when HOLDIR includes spaces.
|
#
253381d9 |
|
24-Feb-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
Force --gcthreads=1 on poly invocations (in crudest way possible) Closes #146
|
#
331d321e |
|
15-Jan-2014 |
Michael Norrish <michael.norrish@nicta.com.au> |
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.
|
#
299c76d4 |
|
01-Dec-2013 |
Michael Norrish <michael.norrish@nicta.com.au> |
Updated version number in manuals, banners etc.
|
#
0254bd45 |
|
22-Nov-2013 |
Magnus Myreen <magnus.myreen@cl.cam.ac.uk> |
removed -lgmp flag
|
#
2fb440a7 |
|
21-Nov-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
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.
|
#
efa86212 |
|
21-Sep-2013 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Tweaks following release of Poly/ML 5.5.1.
|
#
2a28c899 |
|
04-Dec-2012 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|
#
45f59907 |
|
04-Nov-2012 |
Michael Norrish <michael.norrish@nicta.com.au> |
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.
|
#
47d4b651 |
|
18-Sep-2012 |
Anthony Fox <anthony.fox@cl.cam.ac.uk> |
Avoid linker warning messages on Mac OS for Poly/ML 5.5.
|
#
7d7a664c |
|
24-Oct-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|
#
b65d78a7 |
|
04-Sep-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|
#
965007c8 |
|
30-Aug-2011 |
Ramana Kumar <ramana.kumar@gmail.com> |
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.
|
#
2fad30c5 |
|
29-Aug-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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).
|
#
d151d3f7 |
|
29-Aug-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove muddy-related stuff in poly's configure.sml that was commented out.
|
#
53a23ba6 |
|
17-Aug-2011 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update version numbers now that K7 is out.
|
#
f8d4f895 |
|
08-Sep-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Bump version numbers - next release to be 'Kananaskis-7'.
|
#
a0f38493 |
|
09-Apr-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Addition of POLY_LDFLAGS_STATIC variable. This variable is used for static linking whereas the recently added POLY_LDFLAGS triggers dynamic linking.
|
#
e28a1252 |
|
07-Apr-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Store (calculated) Poly/ML linker flags into Systeml. This allows build to read these flags from Systeml, rather than having to recalculate them.
|
#
6b86c491 |
|
06-Feb-2010 |
Ramana Kumar <ramana.kumar@gmail.com> |
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.
|
#
12ee6ed4 |
|
14-Jan-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Apply bits of Thomas's last Emacs mode update (7597) that are OK.
|
#
df77cbf3 |
|
14-Jan-2010 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|
#
2d3dd440 |
|
02-Jan-2010 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Added support for calling Holmake to hol-mode. Moreover, some more key-combinations were added.
|
#
7337074f |
|
07-Nov-2009 |
Peter Homeier <palantir@trustworthytools.com> |
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.
|
#
7b7fe9be |
|
17-Sep-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.)
|
#
58f9662f |
|
29-Jul-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
From now on we're in the Brave New World of Kananaskis 6.
|
#
81d58749 |
|
12-May-2009 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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).
|
#
1a9377a3 |
|
01-Oct-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Put a variable ML_SYSNAME into the Systeml structure recording what ML implementation is being used.
|
#
6564166f |
|
01-Jul-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
More fixes for the poly version - I think this should now let the emacs mode be used with both.
|
#
9d9cd5f2 |
|
01-Jul-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Put a toggle_quietdec function into the Systeml structure, allowing a common interface to be relied on by the emacs mode.
|
#
7dd6e660 |
|
30-Jun-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|
#
dd2caf90 |
|
29-Jun-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|
#
b557dcbd |
|
29-May-2008 |
Scott Owens <Scott.Owens@cl.cam.ac.uk> |
Trivial changes.
|
#
5813e494 |
|
29-May-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove need for poly-tools to have its own mlyacc directory.
|
#
240b34fb |
|
29-May-2008 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
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.
|
#
ad0e7ab1 |
|
29-Apr-2008 |
Scott Owens <Scott.Owens@cl.cam.ac.uk> |
Improve the building process under Poly/ML.
|
#
7966d692 |
|
21-Apr-2008 |
Scott Owens <Scott.Owens@cl.cam.ac.uk> |
A little more polish on the PolyML build.
|
#
c7450402 |
|
21-Apr-2008 |
Scott Owens <Scott.Owens@cl.cam.ac.uk> |
Streamline the PolyML compatibility support a bit.
|
#
80382555 |
|
18-Apr-2008 |
Scott Owens <Scott.Owens@cl.cam.ac.uk> |
Misc fixes to Poly ML compatibility.
|
#
445073c5 |
|
17-Apr-2008 |
Scott Owens <Scott.Owens@cl.cam.ac.uk> |
PolyML compatibility. See tools-poly/README.
|