#
d471fdd7 |
|
13-Nov-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make $< and $@ expand to text of targets/dependencies as written With change to multidir Holmake these were incorrectly expanded to versions with full directory paths attached. Also make the "target" or "dependency" type more abstract, giving it a sub-structure implementation inside Holmake_tools, and generally preferring ‘tgt’ names to ‘dep’ ones. Closes #752
|
#
0d1344de |
|
29-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Holmake: 3 conflated changes - make recursive-build more sensible (it now builds the default targets in every visited directory, not absolutely everything), and only has an effect if the top-level call didn't specify explicit targets. - improve cleaning: this doesn't need to build a dependency graph - better information as directories are traversed by the "recursively" workhorse function
|
#
1bac4c63 |
|
25-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix Holmake's behaviour with --no_prereqs option Now, start with the correct targets, and then adjust dependency graph to turn non-local Pending status nodes into either Succeeded or Failed depending on whether or not the files exist.
|
#
dbf9fb36 |
|
24-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix bug whereby --holstate options on command-line weren't heeded
|
#
2112189c |
|
23-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Now think that handling of HOLHEAPs is probably roughly right
|
#
1caa3b14 |
|
22-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Multi-dir building seems basically done Remaining problems: - output is pig-ugly, because full paths are printed out all over the place - HOL_HEAPs are wrong - .hollogs are not put in the right place
|
#
4d17d639 |
|
22-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Multidir progress Big refactor in progress, making most things into "deps" which are pairs of canonicalised directories and Files. Have also extended control of debugging: can now either turn off particular categories of message, or specify a list of categories to include.
|
#
12993968 |
|
17-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Progress - better diagnostic control - recursions work OK; problems with 1. HOLHEAPs, and 2. dependencies arising through dir1/foo.uo --> dir2/bar.uo --> dir3/fooScript.sml chains
|
#
62e22e55 |
|
17-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Some recursive builds now work correctly
|
#
3a08e8cb |
|
16-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Progress: now some recursive building happens occasionally
|
#
9f0b3052 |
|
16-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Progress: Holmake now builds core HOL (no INCLUDES specs are used) (The build programs choreographs successive calls to Holmake in the various src directories in the right order.)
|
#
bad130f1 |
|
16-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Further progress; mostly right behaviour in single directories Doesn't currently compile but it has recently done so
|
#
adc6bcd4 |
|
15-Oct-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Initial work on multi-dir Holmake - calculate dependency graph for all possible targets at once, moving/isolating the recursion over the directory structure into this process rather than having it govern the building. Intention is to have the complete graph then drive the selection and execution of build tasks - some changes to the DepGraph data type to support this - Holmake.sml is gutted and doesn't all compile, so all of this is untested
|
#
c0e7ee19 |
|
25-Feb-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add directory field to dep. graph nodes This is a first, easy, step towards having Holmake work over multiple directories at once.
|
#
d1fa3077 |
|
26-Feb-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Get Holmake -n not to crash when printing absolute paths With test. Closes #611
|
#
b9ac929e |
|
25-Feb-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Add directory field to dep. graph nodes This is a first, easy, step towards having Holmake work over multiple directories at once.
|
#
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
|
#
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.
|
#
18d1c2f7 |
|
20-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Enable multiplexed builds for Poly/ML Output is horrendous at the moment
|
#
50c4d56b |
|
18-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make dep. graph store single commands per node This is something of a reversal of 8f7f1c9; but there I was worried about smashing multiple commands into a single string, which is clearly still a bad thing to have happen. The problem with having multiple commands in a single node is that a multiplexing implementation has to execute them as an atomic block, which I don't like.
|
#
6cde3a53 |
|
12-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make dep graph record file-name in dependency link Nodes in the graph are commands that may build multiple targets at once. Nonetheless, other nodes may only depend on one of those targets, so we can record this on the arc from the target to the dependency.
|
#
8f7f1c9a |
|
12-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Make dep-graphs store commands as lists of strings This will make it easier to extract and act on leading indicators such as @ and - on each line. If a line is -command then it could be passed to the shell as command ; true. If the command has the leading @, then that line shouldn't be echoed to the shell. In a parallelised context, I'm not sure that anything much should be echoed to the user anyway. Previously, I had Holmake concatenate the lines from the Holmakefile with intervening semicolons, which would just make extracting the @ and - characters that much harder.
|
#
d716a370 |
|
05-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix dep-graph's handling of rules with >1 target Now such rules (including the implicit/built-in rule that builds <n>Theory.sig and <n>Theory.sml from one invocation of a script file), only generate one node in the dependency graph. Actually, the code will treat foo: deps command bar: deps command as if they were written foo bar: deps command because the former is what the latter expands into.
|
#
dd5f56c5 |
|
04-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement a -n option for Holmake This uses the new dependency graph technology. It doesn't look particularly pretty at the moment, but Holmake -n -q should be useful. (The -q suppresses useless info about automatic dependency analysis.) Closes #283
|
#
b5682d77 |
|
03-Apr-2016 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Implement dependency graph type for Holmake This should feed into process-multiplexing for the planned -j feature. It may even be possible to get something reasonable happening here in Moscow ML. Creating the dependency graph should also allow implementation of a -n option (see github issue #283).
|