Wikiproofs:JHilbert development

From Wikiproofs
Jump to: navigation, search
JHilbert development
This page is for discussing the actual implementation of JHilbert, as opposed to its specification or formal description.

The JHilbert proof verifier is not perfect, and we can use the help of software developers to help fix it. This page contains some tips on downloading, building and running JHilbert, some incremental improvements which build on the current JHilbert implementation, and some larger projects and longer-term visions as well. There is no shortage of projects, so please dig in if you see anything which interests you, or ask at WP:TEA if you have any questions.

Downloading, building and running JHilbert[edit]

The JHilbert source code is on github (also see the fork of jkingdon) and contributions are certainly welcome.

Tests[edit]

You can use Wikiproofs as a testsuite, by downloading the wikiproofs content here and then running JHilbert on it (java -jar jhilbert.jar --wiki). Everything should verify except where flagged by Template:error expected, which JHilbert when run with --wiki looks for and then expects it to fail.

Projects[edit]

Here are a few ideas, but feel free to work on whatever strikes your fancy.

  • Wikiproofs:JHilbert definition soundness (the thinking as of 2012 seems to be that two replacement features are needed, abbreviations as described at Help:JHilbert and definitions which are closer to what you'd see in ghilbert versions from 2011 or newer, or something along those lines).
  • Expand the testsuite
  • Make it possible to run the verifier with --wiki on all files in one command. This is expected to be significantly faster than writing a loop as a shell script and invoking jhilbert on each file, because it would avoid java startup time.
  • (somewhat related to the previous) Make --wiki write output such as "processing file xxx" and the like to a log file, reserving standard output/error for errors (and probably a much smaller number of messages).
  • Specifying non-distinct variables instead of distinct variables, as described at User:Norm
  • Implement precedence so we don't need so many parentheses.
  • Provide a way to handle syntaxes like 〈a, b〉 instead of (orderedPair a b) or { a | φ } instead of (abstract a φ). Not clear how general this can be and not introduce ambiguities or excessive complexity, but it would be something along the lines of turning 〈a, b〉 into (〈,〉 a b) and { a | φ } into ({|} a φ). Perhaps the new syntax would need to start and end with constant strings rather than variables, as in the above examples.
  • Profile JHilbert and figure out whether it could be faster (probably yes).
  • What are your thoughts? Feel free to ask on the talk page for input.

If a new feature has a clear migration from the existing wikiproofs (such as requiring a new syntax to enable it which could be used on some, but not all, pages), that is generally a good thing and probably possible in most cases, but we're also willing to require wikiproofs pages to be edited if there seems to be a clear advantage in a feature which requires that.

Plan of action[edit]

The current JHilbert implementation is in a bit of a sad state for the following reasons:

  • Broken definition mechanism.
  • Ugly output (no fancy typesetting, no Lemmon output, etc.).
  • Ugly input (the dreaded infix hack, very constrained grammar).
  • Conflated. It started out as a command line application, and then the Wiki/multithread/network support was brutally hacked into it.
  • Divergence from Ghilbert. This was in part voluntary. But since Ghilbert is currently being redesigned, now would be a good time for some convergence attempts.

So a refactoring is in order, which will probably mean rewriting JHilbert in large parts. Ideally, all of the above issues should be addressed. This suggests the following TODO list:

  1. Decide on a new definition/abbreviation mechanism.
  2. Prove soundness of the new mechanism.
  3. Implement the new mechanism.
  4. Fix all the other stuff ;)

Hilbert C kernel[edit]

The issues above seem to fall into two categories: the stuff that affects the metalogical heart of JHilbert (definitions/abbreviations) and the other stuff (typesetting, charset stuff, etc.). Now, this may sound heretical, but I propose to separate the metalogical heart from everything else. This way, the metalogic behind JHilbert (and possibly variants) could be integrated in the most diverse kinds of software: command line tools, Wiki backends, web applications, maybe even circuit verification software. It seems reasonable to write the, let's call it "Hilbert kernel" in ISO C, for it's fast, portable, and integrable with many other programming languages (insanely enough, this seems even to be true for JavaScript). This kernel would only contain the metalogical core principles and would thus be easy to test. In particular, this kernel would provide an API that is

  • In/Output-agnostic: no-side-effects functions, all in/output is made by the frontend.
  • Charset agnostic: name comparison and hashing is user provided.
  • Storage agnostic: all data structures are created, manipulated and queried in-memory.
  • Multithread-friendly: while ISO C does not know threads, the API can be specified in a thread-friendly way. For example, a module object might have a "finished" flag. In unfinished state, the module object cannot be used for param, import, and export. In finished state, it can be used so, but becomes essentially read-only. One cannot go back from finished to unfinished state.

The kernel could be compiled into a library, like libhilbert.so, or simply be included into some other project as a bunch of C files.

I've started a C kernel library implementation on github.--GrafZahl (talk) 22:00, 27 February 2011 (UTC)

--GrafZahl (talk) 17:58, 5 March 2010 (UTC)