#
e31c304c |
|
07-Oct-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Give buildheap+Holmake --mt c/line opt for control of thread count
|
#
1c9452f4 |
|
14-Jun-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix bug where Holmake would die with Subscript exception Issue was terminal environments where `stty size` and/or `tput cols` (these are Unix shell commands) would return suggesting that the width of the terminal window was 0. Fix the getWidth function to not allow this. Preserve a diagnostic message in poly/BuildCommand.sml that was of some help in tracking this down.
|
#
a586f82f |
|
30-May-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Ensure that non-producing script files get reported even in parallel Test-case checks Holmake output, and exit-code. Rather than having problem-detection in the monitor that sits above the various worker-threads, make the worker-threads detect the problem through a new -c option to the all-purpose buildheap tool. Closes #451
|
#
4ba33079 |
|
16-Jan-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Holmake improvements (bug in caching of dep. analysis; diag change) Two intertwined patches (bad form I know): 1. Fix the bug in tests/indepchildren. 2. Revise the internal diag function to take a function generating a string rather than a string; then the work of generating the string only happens if diagnostics have been asked for.
|
#
c4493862 |
|
11-Oct-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Put a --gcthreads=1 c/line option back into script-building This fell out when I switched things around in the buildheap/script-building infrastructure and may explain the increased incidence of Mk_comb errors being seen.
|
#
1a657356 |
|
14-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Pass Holmake's --dbg flag onto calls to buildheap
|
#
76363081 |
|
13-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Ensure that --relocbuild doesn't cause rebuild on normal follow-up The buildheap executable has to be allowed to be permanently newer than the things it generates.
|
#
cbb3056e |
|
11-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix Holmake deps to point at buildheap rather than poly executable Also remove explicit mention of buildheap from the Holmakefile that builds the first heap. Having it there explicitly prevents a relocbuild from working.
|
#
e5006469 |
|
07-Sep-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get selftests to work again (really: get "HOLMOSMLC" to work)
|
#
a97c5115 |
|
31-Aug-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Attempt to manage all heap interactions in one executable System builds non-interactively, but the interactive REPL is broken, as are selftest.exe files after hol.bare.
|
#
f3b969de |
|
29-Aug-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Stop relocbuild causing rebuild when poly itself is fresh I believe this may have caused issues at the PLDI CakeML tutorial.
|
#
d56fd8b3 |
|
22-Aug-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Update Holmake to cope with Theory.dat files No tests specific to that feature yet. Still also need to update for Moscow ML.
|
#
46ee3d3e |
|
13-Jul-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Allow an indication of side-products of theory builds Basically, write something like foo: *theorynameScript.sml to indicate that foo will be built when the theory theoryname is built. As part of the process, provide much better testing of the parallel execution of multiple target rules and completely change the way these are handled. In particular, the dependency graph that Holmake maintains now does not have multiple targets for a single node, but instead makes sure that when a command is executed for a single target, all nodes that would execute the same command are considered to be running at the same time, and get the same success/failure status when the command finishes. Needs documentation, but is progress with Github issue #429
|
#
5765cb0a |
|
12-Jun-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make script failures actually cause Holmake failures The shell-script needs a set -e line at the top to stop poly failures from being ignored.
|
#
494a77d4 |
|
12-Jun-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Give more diagnostic output in shell-script that builds thy scripts This is not unhelpful in itself but is more of an experiment to try and diagnose the issues Ramana is having.
|
#
66ac9175 |
|
19-Apr-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Read .holpath directories to allow relocatable developments If there is a .holpath file in a directory containing a string with a name for the development under that directory, then the object files (.uo and .ui) in that directory will be easily relocatable because they won't use absolute paths, but will instead use $(devname)/ type paths. Multiple developments can combine in this way, and there is additional machinery to make sure that all of the relevant directories are scanned before reading and writing of object files happens.
|
#
7485218f |
|
18-Apr-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make multibuild Holmake pass on reloc environment variable
|
#
140144ea |
|
18-Apr-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make j1 Poly build pass on environment variable to sub-shells Also rename reloc_build to relocbuild internally (making SML variable name match command-line option name).
|
#
e70eeae7 |
|
12-Apr-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Write and read .uo/.ui files using the $(HOLDIR) variable This should make HOL installations portable (once heaps are rebuilt).
|
#
6607ce61 |
|
29-Jan-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Ensure all .ui files get (faked) old timestamp when reloc-building When a bare .sml file is compiled, an empty .ui file is generated to accompany the .uo file. This needs to also have a faked time-stamp if relocation building is to work.
|
#
a870a911 |
|
23-Jan-2017 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Rebuild .uo and .ui files without forcing unnecessary extra work This is by analogy with what has already been attempted for heaps, and is progress with github issue #105. Also fix a bug with the heap handling if the heap was in a directory with script-files (not the case with the heaps in HOL/src): the dependency graph built for the directory spotted that there was a dependency from the heap to the script files, and even though the heap's time-stamp was set appropriately, the existence of the link in the graph meant that the rest of the graph got executed. The fix for this (in both the case of the heap and the .uo/.ui file) is for execution of graph nodes to check at the time the node is made ready to execute if the target really does need to be redone (by examining time-stamps). Then, the rebuild can be skipped even though the initial analysis thought it was going to have to happen. Future work: - For the moment, both build and Holmake rely on having a particular environment variable set to enable this option. I will augment and/or replace this with command-line options. (The buildheap program needs to retain this use of the environment variable though because neither Holmake nor build control how that program is called; instead this program is called by the user via Holmakefiles.) - Build needs to take an option to clean a HOL installation of its heaps and ui/uo files. I don't know how to automatically identify the heaps, but could just purge those that are identified as such in Holmakefiles.
|
#
e4875d88 |
|
01-Aug-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Allow users to specify time-limit on command-line Thus, Holmake -t10 will kill any sub-process (e.g., a script file running) that doesn't do anything (= produce any output) for 10 seconds.
|
#
6436b454 |
|
05-Jun-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Handle opentheory tgts when building in parallel
|
#
bd86c2f5 |
|
03-May-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Improve error-reporting in -j1 Holmake Includes more error messages when --dbg is set
|
#
f8216ece |
|
28-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make Holmake -j1 output look more as it did before In particular, restore the line about "Linking fooScript.uo to produce ...", even if this now is also preceded by "Holmake: ". With -j>1, this line is unnecessary.
|
#
c3e8b3e5 |
|
21-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Improve reporting of targets with no rules/cmds
|
#
dfc7853d |
|
21-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Report files that can't be built for lack of rule
|
#
20eb6cc0 |
|
21-Apr-2016 |
Michael Norrish <michael.norrish@nicta.com.au> |
Make parallel Holmake's output prettier When a process fails, a chunk of its output up to the failure point is output to the main screen. Also, a process that is killed because of a general desire to give up (a failure elsewhere and no -k option, say), now gets a red M-KILLED ("monitor killed") report.
|
#
1b99daf6 |
|
20-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Finish implementing multibuild for Poly/ML Holmake It doesn't yet look as pretty as I'd like it, but the basic functionality is there. The default parallelisation is 4-way. If you want the old behaviour and look, call Holmake -j1
|
#
18d1c2f7 |
|
20-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Enable multiplexed builds for Poly/ML Output is horrendous at the moment
|
#
8c7d50da |
|
14-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix Holmake under Poly/ML Two significant changes required: * the dependency graph now records nodes for files that already exist and don't need rebuilding. The graph marks such nodes as Succeeded. This gives nodes that depend on these files extra things to point to, giving them a more complete picture. This change also simplifies the code for building the dependency graph in the first place, but is possibly redundant given the second change... * Before "compiling" a source-file, the Poly/ML implementation runs the Holdep analysis on that source file in order to get a better picture of its dependencies stored in the corresponding .uo or .ui file. This is necessary, because the preliminary dependency analysis may be done before the source file even exists. (E.g., fooTheory.sig may not exist when Holmake first starts work in a directory.)
|
#
b6dd58ef |
|
14-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get "build from graph" Holmake to compile Poly/ML version fails miserably at boolScript hurdle however.
|
#
4121aab1 |
|
13-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Start to implement building from dependency graph This code is as yet unconnected to any execution, and is attempting to replicate the behaviour that we have at the moment (corresponding to what will eventually be -j 1). Slightly adjust some types along the way, including changing a bool*bool*string tuple into a record that identifies what the bools are.
|
#
52682c25 |
|
12-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add unused API to build targets from dep. graph
|
#
d2e8537d |
|
06-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Give BuildCommand a shared signature This code is called from the common code of Holmake.sml so it must export the same signature whether it is in Poly/ML or Moscow ML. That signature is useful documentation and sanity-check.
|
#
7b43df0a |
|
30-Mar-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Remove diffs between poly and mosml Holmake impls Next step is to actually remove as much as possible of the tools-poly/Holmake directory.
|