generate consistent app identifier for Isabelle templates

The generated Isabelle theories and ROOT file need to refer to each
other by filename. This commit modifies the tool and build system to
generate a consistent identifier (based on the app name) and pass that
to all the Isabelle templates. This avoids having to hardcode
assumptions about the build system inside the templates themselves.

Isabelle templates: use Isabelle2018-style import syntax

Isabelle templates: support connectors with multiple from/to ends

templates: consistent messages for generated-file warnings

restore 'outfile' context as 'outfile_name'

Isabelle theory templates need to know the output filename. Hence, we
provide the filename as 'outfile_name' when running non-code templates.

trivial: better error message in template

Provide explicit theory names

This fixes these theories that were broken when `options.outfile` support was removed
from templates. The new theory names should be equivalent to what was being derived
previously from the outfile name, although if the Makefile template is changed to
generate different file names then these need to be manually updated.

Document outfile deprecation in theory files

The 'outfile' is being removed as an option templates can query, as a result these templates
will break. Adding this comment is meant to aid understanding if someone attempts to use
these theories before they can be fixed.

Fix licenses

Address some of the more egregious whitespace in CIMP base.

This commit cherry-picks 3cd521a074df61ff0fd4b1a99e09c62a70135195 from
ssh://github.inside.nicta.com.au/mfernandez/project.

Use TPP's condense liberally in CIMP base.

This commit cherry-picks ce3540bd2fe854e85cb5ced79dd5ea71686e78b2 from
ssh://github.inside.nicta.com.au/mfernandez/project.

Remove some unnecessary uses of `joiner` in CIMP base.

This commit cherry-picks f594b2b017bc0c1b7744edea645b07864e1ca818 from
ssh://github.inside.nicta.com.au/mfernandez/project.

Remove duplicated from_instance cases in CIMP base.

Copy and paste error? This also fixes some odd references to undefined
variables.

This commit cherry-picks ef3f0f67f91b0f3b1d14df68b923ae8b40d018d8 from
ssh://github.inside.nicta.com.au/mfernandez/project.

Fix malformed type construction in CIMP base.

This looks to have been a latent bug that we happened never to trigger.

This commit cherry-picks f3a04d40fda186fc6ab205469be859087ff8b03f from
ssh://github.inside.nicta.com.au/mfernandez/project.

Fix use of `embed` in CIMP base.

Apparently this is now a keyword. Hm.

This commit cherry-picks 31d00dd6b8988e2a637fd2672291cc510a604a54 from
ssh://github.inside.nicta.com.au/mfernandez/project.

Fix incorrect use of `children` in CIMP base.

Apparently this was never updated to reflect the new AST.

This commit cherry-picks 166d13aa1c47aef30d46c56cd7957468f99180fb from
ssh://github.inside.nicta.com.au/mfernandez/project.

Fix deprecated use of isub in CIMP base.

This commit cherry-picks 584cd6c2a0f199699c62e8f6782f5aa5f706df17 from
ssh://github.inside.nicta.com.au/mfernandez/project.

Make CIMP base theory runnable anywhere.

This commit cherry-picks 1c59daa319ed62564c1d41cd11cf28f2ce0e990c from
ssh://github.inside.nicta.com.au/mfernandez/project.

Refactored parser init commit.

Throw generation-time exceptions when dealing with unsupported types.

This older verification template was using a textual marker to indicate
unsupported types. The result was that, instead of a generation-time failure,
your eventual proof would fail with a syntax error. This was a little unclean
and also led you to discover the failure much later in your workflow. This
commit cleans it up into a generation-time exception like other such cases.

Trivial: Make some checks against `None` more explicit.

Templates: Access `splitext` through `os.path`.

Templates: Use explicit comparison when testing against `None`.

This is slightly clearer and safer.

Templates: Use `composition` in preference to `me.composition` where possible.

Just for brevity. Should have no user-visible effects.

Remove use of `Joiner` in CIMP template.

JIRA CAMKES-357

Remove AST type `Direction`.

This AST object was not gaining us anything as you always needed to look at its
content to do anything with it. In the templates it was inducing strange code
of the form `p.direction.direction`. This commit removes the type entirely. RPC
parameter directions are now represented as bare strings.

This also relevant in movement towards JIRA CAMKES-334.

Change template license headers to Jinja comments.

The effect of this is that they do not appear in generated output, which was a
bit confusing previously.

Closes JIRA CAMKES-319

Conflicts:
camkes/templates/autocorres/AsynchNativeFrom.template.thy
camkes/templates/autocorres/AsynchNativeTo.template.thy
camkes/templates/autocorres/RPCSimpleFrom.template.thy
camkes/templates/autocorres/RPCSimpleTo.template.thy
camkes/templates/autocorres/SharedDataFrom.template.thy
camkes/templates/autocorres/SharedDataTo.template.thy
camkes/templates/echronos/eChronosAsynch-from.template.c
camkes/templates/echronos/eChronosAsynch-to.template.c
camkes/templates/echronos/eChronosDirectCall-from.template.c
camkes/templates/echronos/eChronosDirectCall-to.template.c
camkes/templates/linker.lds
camkes/templates/linux/component.template.c
camkes/templates/linux/component.template.h
camkes/templates/linux/linuxMQ-from.template.c
camkes/templates/linux/linuxMQ-to.template.c
camkes/templates/linux/linuxMQEmpty-from.template.c
camkes/templates/linux/linuxMQEmpty-to.template.c
camkes/templates/linux/linuxMmap-from.template.c
camkes/templates/linux/linuxMmap-to.template.c

Release snapshot