Tweak releasing-hol script to DTRT with first use of --reusecommit

Correct bugs in 9b07f9609

Sense of test was wrong and there was a syntax error. But apart from
that it was fine.

Try to make sure GNU tar is used on MacOS when releasing HOL

Fix releasing-hol script for a couple of minor changes

1. to account for src/pair -> src/coretypes
2. to not reconfigure when the --reuse-checkout flag is given

Make sure that needed files in bin are in generated release tarball

Thanks to Chun Tian for the bug report

Fix releasing-hol script for kananaskis-11

In particular, the way the Description manual needs polyscripter built
means that releasing needs to build a complete copy of the system at
the correct commit.

Start of a developers' manual.

Progress with #290

Some prettification of the releasing-hol script's output.

Modify release script to work with markdown release notes

Now the HTML file that will eventually appear on the website is
generated with pandoc as part of the script.

Polish releasing-hol script a little.

Fix bug in filenames for released manuals.

Also make the diagnostic output of the releasing-hol script a bit
prettier.

A revised release script now that we use git.

The developers/deleted-in-release.txt lists those bits and pieces that
shouldn't be distributed. This is mostly intended for examples that
are no longer working, or which are still to be made to work.

New option to releasing-hol, allowing library path to be specified.

Allow releasing-hol to pull from a different subversion repo.

This is useful if one has a local cached copy of the repository, which is
something you can set up with the svnsync program.

Also, make a failure to copy in a theory-graph cause the process to give up
there and then.

Tuned.

Bug fixes in releasing-hol script.

A new and updated release tar-file generation shell script, and also a
slight change to the poly code for the Doc2Tex program (doesn't need
to refer to the Systeml module). The releasing-hol script doesn't
bother to build "sub-manuals".

Remove more (object) files that shouldn't be in the tar file.

Preparations for release of k-4. Adjust the name of the repository machine
(it is now hol.cvs.sf.net rather than just cvs.sf.net), and remove the
creation of the HolBdd and HolSat documentation files as these are
now just part of the Description. Also create the new Logic manual, which
used to be part of the Description.

Some last minute changes to get release to work.

Remove the miller example (which doesn't build, and which Joe wants to
get working for next release).

Also copy across the string theory's theorems; for the moment the string
Manual lives...

Further fixes to get generated theorems into system builds.

Updates to releasing-hol to
* allow easy update of "sub-manuals" that are to be built (using the
extra file submanuals)
* build a proper word manual with theorems included from the local
installation (which must be present if you are running this script
at all). See that I will have to do similar things for other manuals
with attached theorems.
* some robustification and generalisation.

----------------------------------------------------------------------

Committing in new version of releasing-hol, which correctly builds the
non-standard documentation for the n_bit library. The non-standard
part is that the library is named "n_bit" but the documentation is
named "word.{dvi,pdf}".

The documentation is renamed to "<version>-n_bit.{dvi,pdf}" for the
exported, public Kananaskis-3.

Anthony, please review this and let me know if you would like some
corrections.

Modified Files:
releasing-hol
----------------------------------------------------------------------

----------------------------------------------------------------------

Committing in a new version of releasing-hol that includes making the
documentation for the n_bit and quotient libraries.

Modified Files:
releasing-hol
----------------------------------------------------------------------

----------------------------------------------------------------------

Committing in revisions to several libraries so that the documentation
builds, and is then presented at the top level when the exported version
of HOL4 is built (as for the public version we are about to release).

This documentation is obviously very much out of date, and yet it still
is greatly useful for people who wish to use these libraries. While
waiting for fully updated versions, I believe this is far better than
not including these, as much of the content does not appear elsewhere.

Modified Files:
hol98/developers/releasing-hol
hol98/src/num/arith/Manual/Makefile
hol98/src/num/arith/Manual/entries.tex
hol98/src/num/reduce/Manual/Makefile
hol98/src/num/reduce/Manual/index.tex
hol98/src/num/reduce/Manual/reduce.tex
hol98/src/pair/Manual/Makefile
hol98/src/pred_set/Manual/index.tex
hol98/src/res_quan/Manual/Makefile
hol98/src/string/Manual/Makefile
hol98/src/taut/Manual/Makefile
hol98/src/unwind/Manual/Makefile
hol98/src/unwind/Manual/entries.tex
hol98/src/unwind/Manual/index.tex
hol98/src/unwind/Manual/unwind.tex
hol98/src/word/Manual/Makefile hol98/src/word/Manual/index.tex
Added Files:
hol98/src/string/help/defs/ASCII_DEF.doc
hol98/src/string/help/defs/STRING_DEF.doc
hol98/src/string/help/defs/``_DEF.doc
hol98/src/string/help/defs/ascii_ISO_DEF.doc
hol98/src/string/help/defs/ascii_TY_DEF.doc
hol98/src/string/help/defs/string_ISO_DEF.doc
hol98/src/string/help/defs/string_TY_DEF.doc
hol98/src/string/help/thms/ASCII_11.doc
hol98/src/string/help/thms/NOT_EMPTY_STRING.doc
hol98/src/string/help/thms/NOT_STRING_EMPTY.doc
hol98/src/string/help/thms/STRING_11.doc
hol98/src/string/help/thms/ascii_Axiom.doc
hol98/src/string/help/thms/ascii_CASES.doc
hol98/src/string/help/thms/ascii_Induct.doc
hol98/src/string/help/thms/string_Axiom.doc
hol98/src/string/help/thms/string_CASES.doc
hol98/src/string/help/thms/string_Induct.doc
----------------------------------------------------------------------

----------------------------------------------------------------------

Committing in a modification to developers/releasing-hol that includes
the pred_set library documentation. To make this easier to include
the documentation from several libraries, wrote a script that uses
the library name as the name of the documentation. Moved the
name of the pred_set library documentation from pred_sets.{dvi,ps,pdf}
to pred_set.{dvi,ps,pdf}.

Modified Files:
hol98/developers/releasing-hol
hol98/src/pred_set/Manual/Makefile
hol98/src/pred_set/Manual/index.tex
Added Files:
hol98/src/pred_set/Manual/pred_set.tex
Removed Files:
hol98/src/pred_set/Manual/pred_sets.tex
----------------------------------------------------------------------

Minor fix for this shell-script.

Comments on CVS tags, and some fixes to the releasing hol script for
the next release.

We can't distribute sunrise just yet, so this removes it from the
directory structure from which the tarball is constructed. Of course, the
source code is on S/F for all to see already, but hey.

Tar file we distribute will now have hol as the name of the top-level
directory. We can't easily change the name of the directory in the
repository, but this will do away with another source of "hol98" for users.

It didn't quite build all the HolSat documentation.

This script is becoming ever more useful. It does just the right
thing now to build a releasable tar-ball, I think.

Another silly bug. Shouldn't remove these files from the tar ball now
that they're not generated.

Couple of bug-fixes.

Minor bug-fix. This program runs well as a script, but may need to be
made executable first.

Probably a reasonable script for producing the tar ball that is to be
distributed. I just cut and paste from it as a rule, rather than
actually run it, but it has the right sequence of commands, I think.

Updates and fixes.

Added code to remove .cvsignore files.

Minor changes to get .pdf and .ps files of the Manuals along with the
.dvi when the documentation is built.

More modifications; might almost be in a state where this script could
actually be run as is (with command-line parameter corresponding to
the release name).

Further refinements. Standard distribution will not include any manual
components. But script does copy out .dvi files to /tmp directory
to have something else done to them.

Made the output of the build stage snazzier.

Added documentation building to release build sequence.

Added shell script for producing hol98 release tarball.