Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified path time heuristic: configurable parameters for larger search space;
  2. clarified heuristics toString; add generator description to schedule;
  3. tuned;
  4. add heuristic for non-scheduled (standard) build behaviour;
  5. proper unused nodes;
  6. clarified schedule message;
  7. proper parallel paths;
  8. clarified build schedule host: more operations;
  9. clarified path heuristic;
  10. clarified graph operations in timing heuristic;
  11. merged
  12. added and removed [simp]s
Changeset 79110:ff68cbfa3550 by fabian huch _huch@in.tum.de_:
clarified path time heuristic: configurable parameters for larger search space;
The file was modified src/Pure/Tools/build_schedule.scala (diff)
Changeset 79109:c1255d9870f6 by fabian huch _huch@in.tum.de_:
clarified heuristics toString;<br>add generator description to schedule;
The file was modified src/Pure/Tools/build_schedule.scala (diff)
Changeset 79108:ed00312f694f by fabian huch _huch@in.tum.de_:
tuned;
The file was modified src/Pure/Tools/build_schedule.scala (diff)
Changeset 79107:f5a2f956b531 by fabian huch _huch@in.tum.de_:
add heuristic for non-scheduled (standard) build behaviour;
The file was modified src/Pure/Tools/build_schedule.scala (diff)
Changeset 79106:91955d607aad by fabian huch _huch@in.tum.de_:
proper unused nodes;
The file was modified src/Pure/Tools/build_schedule.scala (diff)
Changeset 79105:6e92475ff925 by fabian huch _huch@in.tum.de_:
clarified schedule message;
The file was modified src/Pure/Tools/build_schedule.scala (diff)
Changeset 79104:e7ab5f4ed401 by fabian huch _huch@in.tum.de_:
proper parallel paths;
The file was modified src/Pure/Tools/build_schedule.scala (diff)
Changeset 79103:883f61f0beda by fabian huch _huch@in.tum.de_:
clarified build schedule host: more operations;
The file was modified src/Pure/Tools/build_schedule.scala (diff)
Changeset 79102:4d5f878665a3 by fabian huch _huch@in.tum.de_:
clarified path heuristic;
The file was modified src/Pure/Tools/build_schedule.scala (diff)
Changeset 79101:4e47b34fbb8e by fabian huch _huch@in.tum.de_:
clarified graph operations in timing heuristic;
The file was modified src/Pure/Tools/build_schedule.scala (diff)
Changeset 79100:e103e3cef3cb by nipkow:
merged
Changeset 79099:05a753360b25 by nipkow:
added and removed [simp]s
The file was modified src/HOL/Boolean_Algebras.thy (diff)
The file was modified src/HOL/Lattices.thy (diff)
The file was modified src/HOL/Set.thy (diff)