Synthetic Philosophy and Deductive Engineering
The project is organised into subsystems each with its own top-level directory, in addition to which there is a docs directory for materials not specific to any single subsystem.
Where there is no compelling reason to do otherwise, documents will be written in github markdown, and will be organised in such a way as to provide a transparent and complete view of the project from the project web site on rbjones.github.io/SPaDE
Documents specific to some subsystem will be in the top-level sub-directory for that subsystem.
High level and project wide documentation will be in the docs directory, which has an admin subdirectory for materials of a non-technical nature.
The general policy on naming of documents is that they should be in numerical series prefixed by short identifiers for the subsystem or subdirectory, and for the kind of document as follows. This seems to be morphing to using the subsystem codes for directories, whether or not they are subsystems, so that the README.doc indexes all the documents with the same subsystem code.
This needs to be made sufficiently systematic for all contributors (including copilot) to be able to choose filenames and maintain README.md files consistently.
Subsystem codes:
YYYYMMDD-HHMM-author-topic.md, see reviews.Document kinds:
After the two prefixes documents will have a three digit number starting at 001 for each kind of document. This completes the basename. Document name extensions will generally indicate the language in which the document is written, or the coding format. In some cases documents will have derivatives whose filename has the same basename but a distinct extension. This will happen when code or formal specifications are included alongside explanatory text in an .md file, or when the processing of one kind of formal text yields some other file (e.g. compiling a source module into an object module). Except in such cases of derivative documents, basenames should be unique. Derivative files having the same basename but a distinct extension should not be linked to separately in the README.md of the their directory.
Document headers should be avoided in markdown pages because of the impact on web page readability and presentation. A footer is more acceptable. Dates need not be included, history can be traced through git logs. The primary author should be indicated, which in the case of copilot should include the model name. Where a document results from conversation with an AI agent a link to the chat log should be included.
In the case of code or formal specifications not embedded in markdown a brief header mentioning authorship, including model name if AI.
This includes:
Guidance for potential and actual collaborators, both human and AI, either in this project or in associated but distinct enterprises,including:
admin/ (apart from one in the .github directory)admin/ directory and will be referred to in the relevant high-level documentsThere was previously an intention to use markdown more exclusively, as in a literate script system, including for formal specifications or code, and at that time the following exceptions were noted. The following exceptions to the policy were then noted, but probably are no longer relevant, insofar as there is no longer an intention to use markdown as a literate programming system.
There may be a small number of papers prepared as if for publication in the proceedings of conferences, in whatever the required format is (normally latex with a special formatting). Where possible these may be constructed using the markdown package to include markdown sources.
Historical material in the retro directory is mostly in .pp files, which are in a ProofPower literate script format normally including both tex source and formal specifications in HOL. These are intended ultimately both for processing by ProofPower and for creating PDF documents using texlive.
It is likely that a compendium of project documentation as a PDF reference manual will be desirable if the development is successful. This would likely be produced by texlive, mainly compounded from .md files incorporated using the markdown package or converted to .tex files using pandoc, with one or more .tex files glueing them together.
These will form the main part of the technical output during the early stages of the project, and will be in ProofPower HOL. They will normally be in literate scripts either as .pp files or as .md files.
It is policy to progress all informal documentation into formal models at all levels. At the lower levels this is part of the reflexive reasoning required to approach the first singular foci and is therefore of high priority. At the higher levels it is probably less urgent.
The reflexive nature of the project architecture means that from the earliest possible stage the abstract representation of algorithms will be in the HOL abstract syntax, and concrete syntax will be supplied as required by LLM like general intelligence in an outer shell. The implications of this for the documentation is not yet clear, but the preference will continue to be to address the needs through descriptions in github markdown documents. First prototyping of the logical kernel are likely to be by transcription from HOL to SML.
When undertaking reviews, please place outputs from the review in a markdown file in the “reviews” directory file in the root of the repository, or in a subdirectory of that directory if the comments relate to a specific subproject. Use a filename which includes the date and time of the review followed by the contributor name, (e.g. copilot). The date and time should be rendered in a formal which collates the files in temporal order in a directory listing, e.g. 20241001-1530-copilot.md for a review made on 1st October 2024 at 15:30 by copilot. A further component of the filename may be a brief indication of the subject matter, e.g. 20241001-1530-copilot-KRreview.md Avoid using colons (:) in filenames as they cause issues with Jekyll/GitHub Pages processing.
This policy will evolve as the project develops and we learn what works best for our collaboration and documentation needs. All changes should be documented and justified based on our experience.