Commit Graph

761 Commits (1ec0fc0c7bae98548fb6d300ddbfe28265a94355)

Author SHA1 Message Date
Mike Gerwitz 1ec0fc0c7b design/tpl (Notational Convetions): Clean up unneeded bicompi
This was originally going to be used to define @yields for the classifier,
but I took a very different approach which doesn't require reasoning about
the system in terms of recursion.
2021-05-18 10:16:06 -04:00
Mike Gerwitz 2d268f2a55 design/tpl: Initial definition of classifications
This defines @as and @yields, but does not yet define matches formally.
It's also missing index entries, which I'll take the time to add after I'm
sure things are staying as they are.

This was quite a bit of work, and the approach I took is different than I
originally expected, so Section 0 can use some cleanup.

There is more to come from here.
2021-05-18 10:09:29 -04:00
Mike Gerwitz 4ea2574a8c design/tpl/tpl.sty: Use autoref for theorem macros 2021-05-17 13:21:56 -04:00
Mike Gerwitz fbe76a5616 design/tpl: Beginnings of classifications in terms of first-order logic
This is going to evolve a great deal, and note that the yield definition is
completely absent.

It may be time to switch to natural deduction (Gentzen-style).
2021-05-14 12:14:11 -04:00
Mike Gerwitz 9bcd7e1d7e design/tpl: Abstract theorem env + label creation 2021-05-14 10:50:49 -04:00
Mike Gerwitz 9fd57872ed design/tpl (Monoids and Sequences): Add missing index entries
Forgot in previous commit.
2021-05-14 10:38:17 -04:00
Mike Gerwitz 8d54420656 design/tpl (Monoids and Sequences): New section 2021-05-14 10:34:13 -04:00
Mike Gerwitz 060a7d0e6c design/tpl: \{log=>l}{and,or}
Don't I feel silly.
2021-05-14 10:34:09 -04:00
Mike Gerwitz 63b502b7df design/tpl: Add ccicons for Copyright line 2021-05-12 10:37:20 -04:00
Mike Gerwitz 1ad6bc93d7 design/tpl (Meta: Typesetting): Correct use of \tameclass
That macro previously expanded into \Classify, but that was undone before
committing to make it clear when one is referring to a variable vs. a
classification as a definition.
2021-05-11 16:52:03 -04:00
Mike Gerwitz 3cb2726737 desgin/tpl: Appendices begin on a new page 2021-05-11 16:50:23 -04:00
Mike Gerwitz bff2b32a52 design/tpl: More TODOs and margin remarks 2021-05-11 16:50:11 -04:00
Mike Gerwitz 9d9535a1b8 design/tpl: Introduce \Classify mathop
This will be used as an IR of sorts to eliminate the XML, which will be far
too verbose to use in proofs.  It also allows us to attach behavior to the
operator, which will end up defining two values for @as and @yields.
2021-05-11 16:37:08 -04:00
Mike Gerwitz d78186461f desgin/tpl: Add \todo margin notes 2021-05-11 16:36:43 -04:00
Mike Gerwitz 08109bc35d design/tpl: Vector addition example: \bicomp{=>i}
The example as presented was incorrect, since \bicomp is undefined for
scalar values.
2021-05-11 13:49:18 -04:00
Mike Gerwitz 7735ba1f29 design/tpl: Remove \exists from classification definitions
The previously-existing notation for this has been removed.  These will be
updated soon to account for vectors and matrices, but until then, this is
simply nonsense.
2021-05-11 13:28:02 -04:00
Mike Gerwitz d49133e8e9 design/tpl: (Disjunctive Classification): Footnote formatting correction
Missing `,' in the \forall set.
2021-05-11 13:24:20 -04:00
Mike Gerwitz 51c87f9938 design/tpl: Reposition disjunctive classification footnote
The original position made it look to much like d^2.
2021-05-11 13:21:05 -04:00
Mike Gerwitz 6dc0ca2454 design/tpl: Show listings in draft mode
What an odd default.
2021-05-11 13:08:25 -04:00
Mike Gerwitz 5808afc8a2 design/tpl: Universal=>conjunctive, existential=>disjunctive classification 2021-05-11 13:06:06 -04:00
Mike Gerwitz 2407af56e4 design/tpl: _-notation clarification (wildcard/hole) 2021-05-11 12:47:28 -04:00
Mike Gerwitz 13317aac6c design/tpl: Vectors and Index Sets \goodbreak
This fits nicely on a single page.  At the time of writing, the previous
section is near the end of the page, so this works reasonably well.
2021-05-11 11:39:23 -04:00
Mike Gerwitz 7f4fc8e3b7 design/tpl: Mostly-complex symbol index entries for Chapter 0 2021-05-11 11:33:12 -04:00
Mike Gerwitz 7624bd2958 design/tpl: TAMER case fix
'T' was lowercased.
2021-05-11 11:32:19 -04:00
Mike Gerwitz 02335f9a4a design/tpl: Clear copyright on Index pages
Apparently index page output uses a different even/odd determination than
the normal article page output.
2021-05-11 11:31:27 -04:00
Mike Gerwitz dfb013ca74 design/tpl: Corrected conjunction/disjunction index placement
They were incorrectly placed at the quantifiers.
2021-05-11 09:59:03 -04:00
Mike Gerwitz cb9ccfe5f3 design/tpl: \vdash=>\infer and index entry 2021-05-10 16:54:19 -04:00
Mike Gerwitz 4e7b882aed design/tpl: Begin symbol list at beginning of index 2021-05-10 16:50:30 -04:00
Mike Gerwitz 176c7785e9 design/tpl: Remove stackengine import
This is no longer needed after conversion of \bicomp to superscript.
2021-05-10 14:29:42 -04:00
Mike Gerwitz c371d12a02 design/tpl: Remove glossary
This is an unnecessary feature to maintain right now.  I will include
symbols at the very beginning of the index, which is common in mathematics
texts, and may will add a table of common symbols in the future.
2021-05-10 14:28:37 -04:00
Mike Gerwitz cacb72b2bd RELEASES.md: Entry for TPL 2021-05-10 14:21:24 -04:00
Mike Gerwitz 8d1c29b4cc design/tpl: bicomp: Use superscript instead of stacking
Stacking originally seemed like a good idea, but perhaps this does read a
bit better (and looks more like the composition operation being applied),
and composes a bit better if we needed e.g. \bicomp\bicomp{R}.

It's also less ambiguous when it's over a larger expression.  For example,
\bicomp{[A]} places \circ over top of the A, which looks as if it's
[\bicomp{A}].  It's obvious what the intention is in that context, since
\bicomp{A} makes no sense, but there could be other situations where it
doesn't.  With this change, it results in {[A]}^\circ.
2021-05-10 14:19:49 -04:00
Mike Gerwitz 0a16808542 design/tpl: Subscript notation for function application
This is convenient and visually appealing in certain circumstances.  That's
highly subjective.
2021-05-10 14:08:11 -04:00
Mike Gerwitz bd454f7a7c design/tpl: The Tame Programming Language initial concept
There's a lot of change that's likely going to take place with this thing,
but it's a start.  The abstract summarizes the purpose of this---to formally
define TAME in terms of algebra, first-order logic, and [ZFC] set theory.

This came about while working on compiler changes and optimizations, since
it's difficult to ensure correctness (and discover further optimizations)
without being able to formally define the language.  The focus at the moment
is the classification system rewrite, which can be expressed in terms of
first order logic and set theory.

This commit contains essentially a POC with some carefully chosen
mathematical foundations (abstractions of which are subject to change) and a
basic representation of a subset of the classification system for scalars.
2021-05-10 13:46:49 -04:00
Mike Gerwitz 685549f06b RELEASES.md: Update for v17.8.1 2021-03-18 09:56:02 -04:00
Mike Gerwitz 56210497ad RELEASES.md: Summary for next release 2021-03-18 09:55:36 -04:00
Mike Gerwitz 43204d1dd5 build-aux/Makefile.am: Lookup table dependency fix
%.xml{=>o}: %csvo rater/core/vector/table.xmlo

That is: we'll only build an object file when we try to build another object
file.  This was causing problems with dependency generation, because it will
triggering compilation early.
2021-03-17 17:02:58 -04:00
Mike Gerwitz 6b35812405 RELEASES.md: Mention recent tame and tamed changes 2021-03-15 09:49:57 -04:00
Mike Gerwitz 6221ce5fee bin/tame (verify-runner): Add missing id param
This was referencing a global $id, which is not the value we are interested
in (and may not exist at all).  Add the missing param.
2021-03-12 14:14:42 -05:00
Mike Gerwitz 7325578624 bin/tame{,d}: Fix assignments that lose exit code
Ensure that we fail if the command in the assignment fails.
2021-03-12 14:14:40 -05:00
Mike Gerwitz e7e4a61cf4 bin/tame: read {=>-r} where missing
While these should not be necessary in practice, there's no reason _not_ to
do this.
2021-03-12 09:47:38 -05:00
Mike Gerwitz 2a56c75345 bin/tame: Remove unnecessary trailing backslashes
This was originally in a Makefile, long ago, where backslashes were
actually needed.
2021-03-12 09:47:34 -05:00
Mike Gerwitz dfce9a89d8 RELEASES.md: Update for v17.8.0 2021-02-23 10:51:59 -05:00
Mike Gerwitz 566d9f6536 build-aux/Makefile.am (suppliers.mk): Regenerate when any sources change
This should have been done many years ago.  This will determine if any of
the dependencies have changed for the included suppliers.mk and regenerate
it as needed, without the developer having to do so manually when imports
change.
2021-02-23 10:48:21 -05:00
Mike Gerwitz cda3e845b8 Remove verbose messages from suppliers.mk generation
* build-aux/Makefile.am (suppliers.mk): Invoke ant with `-q` to eliminate
"processing" messages for each and every file.  This also speeds up
operation slightly.
* build-aux/gen-make: Remove information echos for each file.

These changes will allow for suppliers.mk to be regenerated automatically
without being so invasive.
2021-02-23 10:47:40 -05:00
Mike Gerwitz c319719065 src/current/rater.xsd (yieldsNameType): Remove length checks
The intent originally was to try to keep developers to a reasonable name
length, but generated identifiers can easily exceed this, and we further do
not support namespacing.

This can be handled at a template level instead for enforcing naming
conventions.
2021-02-23 10:46:58 -05:00
Mike Gerwitz 8651f683f6 src/current/rater.xsd: Update
This had gotten quite out of date from the actual rater.xsd, which existed
outside of this repository, that is used during our build process.  That was
an unintended artifact from moving files around.

That file has been removed and symlinked to this one.
2021-02-23 10:46:03 -05:00
Mike Gerwitz 6f67a4d6fa build-aux/Makefile.am: Accommodate step-level packages from proguic
Note: this really belongs in liza-proguic, and should be moved in the near
future.

liza-proguic is being modified to generate step-level packages, which are
significantly faster to build than larger ones (XSLT TAME scales
terribly).  These changes handle those new dependencies.

One important thing to note with this change is that suppliers.mk now
requires proguic to have run before generation so that those generated
dependencies can be properly examined.  This is a quick operation, so that
is not problematic.

This also depends on the .version.xml change that was previously made: when
the timestamp changed every time, we got into an infinite build loop.
2021-02-23 10:44:50 -05:00
Mike Gerwitz 9f5517f0d9 src/current/pkg-dep.xsl: Recognize step-level imports
First thing to note: this belong in liza-proguic, not here.  But it's here
right now, so for now I'm making the change.  The relationship between TAME
and proguic is awkward and will hopefully be improved upon in the near
future.

As for this actual change: step-level fragments will be concatenated such
that the imports will appear at the step level rather than the root.
2021-02-23 10:44:03 -05:00
Mike Gerwitz 80a61986bd build-aux/m4/calcdsl.m4: Do not generate suppliers.mk
This will be generated automatically by the Makefile.  It's not appropriate
to generate in the configure script, and I do not recall why I did
so---possibly to work around the issue of delayed tab completion when it
needs regeneration?

This removes suppmk-gen in favor of more generic Makefile targets---in this
case, having `%.tdat` depend upon `rater/core/tdat.xml`, even though that's
not quite true (the %.xml file generated from it needs it).  But these files
are going away soon; a pending TAME optimization branch removes support for
the underlying pattern primitive entirely; CSVMs should be used instead.
2021-02-23 10:43:09 -05:00