The main restructuring thrust is nearing completion, so let's get rid
of the `restructuring` namespace.

1) rely on patch to actually patch the Makefile
2) move ineffective 'sed' hackery related to 'make validate'

Re 2), the sed script didn't actually modify the Makefile anyway
(unlear how long it has been ineffective), so let's just remove it.

Add support for compiling only classic Prosa, i.e., the inverse of
--without-classic.

No need to re-generate an unchanging file from scratch.

It's faster to just compile the new stuff. For new developments,
that's sufficient.

Also switch how this is patched into the Makefile while we're at it.

...while at it, remove some old cruft in there.

Marco Perronet authored 5 years ago and Björn Brandenburg committed 5 years ago

Add the `htmlpretty` target to the Makefile to generate prettier documentation,
based on the CoqdocJS project.

     https://www.ps.uni-saarland.de/~ttebbi/coqdocjs/

     https://github.com/tebbi/coqdocjs

Many thanks to Tobias Tebbi for creating CoqdocJS.

If one names a branch "something-something-file.v", then the current
script will find it in the .git directory and try to compile git's
branch description as a Coq file...

- Remove Require declarations from Modules.
- Small fixes due to changes in the type checker.
- Generate _CoqProject with Makefile and remove spurious warnings from ssreflect.

The BSD version of `find` needs to be given '.' as the search path.

- Removed unnecessary assumption in RTA about task precedence/no intra-task parallelism.
- Scheduler models and analyses are organized in separate modules/folders.
- Added RTA for FP and EDF for schedulers with release jitter.
- The scheduling invariants were split into more fine-grained assumptions:
  (a) scheduler is work-conserving
  (b) scheduler enforces FP/JLDP priority X
- New helper lemmas about counting, and sorted/uniq lists
- Inclusion of tactics feed and feed_n (see documentation).
- Added a Makefile generator