The Twelf Project:TwelfTag
From The Twelf Project
TwelfTag is Rob's system for non-interactively checking Twelf code. This is a guide to TwelfTag for contributors; if you are a reader, then this article may be more helpful. While Twelf Live allows people to interact with signatures, TwelfTag is designed for writing and checking code for use in wiki articles.
Contents |
[edit] The <twelf> tag for syntax highlighting
The <twelf> tag itself is simple enough, it works much like an HTML <pre> environment with syntax highlighting, and almost exactly like using the <code twelf> tag that does (somewhat broken) Twelf syntax highlighting using a GeSHi plug-in.
However, the <twelf> tag is the only way to access the powerful features described below, utilizes a superior syntax highlighter written in Haskell, and does various other nice things. For instance, it crops out any whitespace at the beginning or end of the environment so that this:
<twelf> exp : type. abs : (exp -> exp) -> exp. </twelf>
Will look like this:
exp : type. abs : (exp -> exp) -> exp.
[edit] The <twelf> and <twelflink> tags
Behind the scenes, the content of every <twelf> tag is grouped together. So if you have a series of Twelf tags that are defining a single signature, like this (continuing from the example above):
app : exp -> exp -> exp.
and this:
step : exp -> exp -> type.
then TwelfTag, at this point in the process, has code for exp, abs, app, and step gathered in a group, though it hasn't done anything with it yet.
[edit] The <twelflink> tag
You can link to a collection of all the code that has been presented so far by using <twelflink> tags in the same way you would use <a href=...> tags in normal HTML code.
As an example, <twelflink>OMG link!</twelflink>, will appear like this: OMG link!, pointing to the four lines of code declared so far throughout the file.
The filenames are just the MD5 hashes of the code which they contain; files in the /w/hcode/ directory should not be assumed permanent at this point, though I don't have immedate plans to create a cleaning system.
[edit] The check="true" option
We are not collecting code in the background just to link to it, we're creating code so we can check it in Twelf! If you create a flag <twelf check="true">, Twelf will execute the collected segments in Twelf and link to the output.
step/app1 : step (app E1 E2) (app E1' E2) <- step E1 E1'. step/app2 : step (app E1 E2) (app E1 E2') <- step E2 E2'. step/appabs : step (app (abs [x] E x) E') (E E').See Twelf's output
You may notice that the link above links to a file "twelf.plparty.org/hcode/<obvious md5 hash>.chk". The code that was checked is just at "twelf.plparty.org/hcode/<exact sameobvious md5 hash>" - that is, without the ".chk".
You can use <twelflink check="true"> to link to the Twelf output of checking the most recent code instead of just linking to that code code - so <twelflink check="true">See?</twelflink> just duplicates the link that was automatically entered in above. See?. This works even if you haven't set check="true" in any of your <twelf> tags; you could just avoid using the check="true" option in your code in favor of causing checks with <twelflink check="true"> calls.
[edit] The check="decl" option
If you want to concentrate on the output of the last code fragment, for instance to examine a particular case of type reconstruction, you can use the check="decl" option for the Twelf tag. In the background, TwelfTag loads the previous portions of the signature on chatter 0, and then returns to the default chatter 3 to run the current code snippet. It then does some simple manipulations on Twelf's response to remove things like useless %% OK %% notices, and then inlines the result.
<twelf check="decl"> test = step/app1(step/app2 step/appabs). </twelf>
test = step/app1(step/app2 step/appabs).Twelf 1.5R3, Aug 30, 2005 (%trustme)test : {X1:exp} {X2:exp -> exp} {X3:exp} {X4:exp} step (app (app X1 (app (abs ([x:exp] X2 x)) X3)) X4) (app (app X1 (X2 X3)) X4) = [X1:exp] [X2:exp -> exp] [X3:exp] [X4:exp] step/app1 (step/app2 step/appabs).
%% OK %%
[edit] The discard option
If you add <twelf discard="true"> then it will syntax highlight but will not incorporate the segment into the collected code.
<twelf discard="true"> % Don't do this! step/appabs : step E1 E2 <- step E1 E2. </twelf>
% Don't do this! step/appabs : step E1 E2 <- step E1 E2.
You can also incorporate the discard= and check= options, for instance to run a query that you don't want to re-run in future.
<twelf discard="true" check="decl"> %solve _ : step (app (abs ([x] app x x)) (abs ([x] app x x))) _. </twelf>
%solve _ : step (app (abs ([x] app x x)) (abs ([x] app x x))) _.Twelf 1.5R3, Aug 30, 2005 (%trustme)%solve step (app (abs ([x:exp] app x x)) (abs ([x:exp] app x x))) X1. OK _ : step (app (abs ([x:exp] app x x)) (abs ([x:exp] app x x))) (app (abs ([x:exp] app x x)) (abs ([x:exp] app x x))) = step/appabs.
%% OK %%
This above example brings up another important point: please don't kill my webserver, for instance by executing the reflexive-transitive closure of ω. I'm not entirely certain what will happen to runaway processes; they won't be able to do much damage, but they certainly won't achieve anything useful. I plan to address this before the site goes public, but I'm not there yet.
(Note: discard="true" used to be noinclude="true", but this changed because it was confusing. The option noinclude="true" still works but you shouldn't use it.)
[edit] The include= and name= options
This is a tricky feature that allows you to run parallel segments of code on a single page. It should be used sparingly, as otherwise it can become extremely confusing to both readers and editors. Each <twelf> tag is associated with a value, include, that defines where it gets its code from, and a value, name, that defines where it binds the concatenation of the code the previous code and the new code within the tag.
- If include= is not defined, it is assumed to be the empty string.
- If name= is not defined, it is assumed to be the value of include. The value of name can only be the empty string if the value of include is the empty string, and the value of name should never be the underscore.
In most cases discard="true" should be sufficient — discard="true" is actually just a derived form of name="_".
This example is hopefully revealing:
<twelf include="nat"> nat : type. </twelf> This is a simple way of expressing nats: <twelf include="nat" name="natsimple"> z : nat. s : nat -> nat. </twelf> This is a verbose way of expressing nats: <twelf include="nat" name="natverbose"> nat/z : nat. nat/s : nat -> nat. </twelf> <twelflink include="natsimple">See the simple code</twelflink> <twelflink include="natverbose">See the verbose code</twelflink>
nat : type.
This is a simple way of expressing nats:
z : nat. s : nat -> nat.
This is a verbose way of expressing nats:
nat/z : nat. nat/s : nat -> nat.
(Note: group="..." used to be roughly the same thing as what include="..." now is. Now group="..." is just an alias for include="...", but you shouldn't use it.)
[edit] The hidden option
You can use the hidden="true" option to insert Twelf into a page without having it appear to the reader. This option works with the include and name options, does not work with <twelftag>, and ignores any check option.
By inserting this code into the wiki you can add a definition of "plus" to the code group named "nat".
<twelf include="natsimple" hidden="true">
plus : nat -> nat -> nat -> type.
plus/z : plus z N N.
plus/s : plus (s N1) N2 (s N3)
<- plus N1 N2 N3.
</twelf>
[edit] Quick check
On edit pages, there is a button labeled "Quick Twelf check" that will check your Twelf code without leaving the edit page. It will collect all of the bare <twelf>...</twelf> code, submit it to the Twelf server, and open a box with Twelf's output right below the button. You may immediately edit the code within the edit window and press the button again to check it again. This currently does not work with the name, check="decl", but it may soon.
[edit] TwelfTag and caching
In order to save resources, TwelfTag only creates a file or checks a signature if a file with the expected hash doesn't currently exist. This is layered on top of MediaWiki's caching system, which doesn't even call TwelfTag if it has a cached version of the page content somewhere.
Therefore, if someone deleted a file from the /w/hcode directory and didn't modify all the wiki files that use it, a visitor to the page would find the code links all broken - MediaWiki would serve the page without allowing TwelfTag to check that the code files exist. The solution to this is to invalidate the Mediawiki page cache. This sounds scary but is easy to do—if you touch /w/LocalSettings.php, it will invalidate every cache that was generated before the touch, and therefore cause the next visit to any given page to re-check that the code for that page exists.
This won't help someone who is already visiting a page when files are deleted—the files won't be recreated until that page is reloaded; therefore, code deletions should only happen at extremely low-traffic periods.
