Update 2006-01-06: Thanks to work by dan, development has now shifted over to the Django framework and the system is now called "Ghestalt" (barGhest alternative). Please go to ghestalt.ghilbert.org and try logging in (if you created an account on the Barghest, it will probably be there on the new system). – raph
Barghest is the (still somewhat mythical) content management system for ghilbert.org, although there is a prototype online with account and wiki functionality at barghest.ghilbert.org. All AsteroidMetans are welcomed to create an account there and play.
The core of the site will be one web page per theorem, just like the Metamath proof explorer. Like Metamath, the terms are to be typeset nicely, and uses of theorems as proof steps will be hyperlinked.
However, there are to be major differences. While the Metamath site is read-only, virtually all of the content on ghilbert.org is to be writable by users. Each theorem, then, effectively has a wiki page for comments and the like. The same goes for proofs-in-progress, for which the page hosts proof fragments, questions for experts, suggestions, and so on.
Minimum requirements include:
Most of these requirements are fairly modest as content management systems go. I'm not looking to reinvent Xanadu here. However, the tight integration with Ghilbert verification and typesetting certainly means that lots of new code is needed. Certainly, there is no existing off-the-shelf system that meets all these requirements.
I'd like to have something online within the first half of 2007. One reason I'm posting this page is to find out whether there's any interest for people here to take on some of the work. From what I read here, many of the PlanetMathers have an interest in building a content management system for a database of mathematical theorems. What's less clear to me is whether they have an inclination to get their hands dirty with the scutwork of a practical system for Ghilbert that's an incremental evolution, or are more interested in pursuing an idealistic vision infused with mathematical elegance.
My inclination is to just start hacking. To keep things simple, the starting system will look something like this:
I'll update this page when I have something online, and the sources checked into my publicly readable darcs repository.
– raph 23 Dec 2006
I'm interested in helping. Been messing around with django lately… anyway, I think this is a worthy project. dan 24 Dec 2006
I wonder if you might want to consider using some basic project management techniques to encourage developers to join up. FYI, There are high-normal people earning $100 - $150 an hour as project managers – and as with other areas of specialization, there are best practices and decades of expertise showing what works and what doesn't.
For example, breaking down the design into logical components, each having specifications.
Also, I would suggest not making (annoying) predictions that other systems will not be operational for "a few decades." – that is just basic psychology if you want to build an effective team.
--ocat
--slawekk
While MySQL may be a pragmatic choice depending on the existing software you will be using, I would like to make known my displeasure with it. I know it is the most common choice for "content management" applications, where you don't mind a few lost transactions here and there, and the data being dirty every now and then. Even slashdot uses it.
While I understand recent versions have improved, MySQL was initially designed as a hack by people who apparently where either unaware of or didn't care about data integrity or RDBMS theory. It would be (or at least used to be) almost suicide to use it for a "real" database application involving thousands of users entering financial transactions, where you are basically at the mercy of bug-free validation in the user and database interface code. Only recently was the concept of transactions, atomic operations, and rollback implemented, as I understand it, and to achieve that you have to use another vendor's storage engine (InnoDB). Until recently, you could not lock a single row, but had to lock an entire table to ensure transaction integrity, locking out all other users for that time period. My comments are based on my evaluation in the early 2000s - others felt the same, e.g. Why Not MySQL? - and even though I understand things have improved, MySQL just left a bad taste in my mouth. Having been previously exposed to real DBs, it seemed to me that even learning MySQL as your first DBMS would poison your mind like learning BASIC as your first programming language. :) For a more current (if still not necessarily unbiased) critique, see Wikipedia's article. As that article mentions, some people also feel there are some software "freedom" issues with the MySQL AB company's code ownership. PostgreSQL, on the other hand, is BSD licensed.
When faced with a choice in the early 2000's for an inventory management system on Linux, where it was absolutely crucial that ledger postings have 100% accurate financial data, I convinced our customer to use PostgreSQL instead of their initial MySQL choice (that's all they had heard of) after researching it. PostgreSQL was designed from the ground up as a real ACID-compliant database, according to the design principles of database theory and strictly conforming to ANSI SQL standards for its query language. All in all, it is simply a beautiful, clean database design, not a hack like MySQL. I think that switching from MySQL to PostgreSQL in the code is pretty simple, especially if you've modularized the DB interface. An issue, I believe, is that porting data from MySQL to PostgreSQL can be a nightmare if the data volume is huge, because data integrity may not have been enforced, requiring a lot of manual cleanup. Converting data from PostgreSQL to MySQL should be trivial if you want to go back, although I haven't tried it. BTW I wrote an extremely detailed "howto" that enabled an inexperienced person with no exposure to Linux to rebuild the system from scratch, starting from formatting the disk, that included the installation and setup of PostgreSQL (as well as Apache/HTTPS and PHP).
The above is just my opinion, and is based on my evaluation in the early 2000's. But I personally would choose PostgreSQL for any new application. – norm 24 Dec 2006
Thanks for your input. The decision between MySQL and PostgreSQL is strictly pragmatic. In Python, it's almost trivial to switch between the two, and web.py's connect() function (in db.py) knows how to open four different kinds of databases.
MySQL has matured six years since your evaluation, it has a vital user community and a serious company behind it (I had the pleasure of meeting several of the developers a few years back), and we have an instance on the Ghostscript server to host our Bugzilla. Further, this application really doesn't need a "real" database with transactions and so on. Maybe if it scales more than a few orders of magnitude, a more serious database will be worth considering, but then it should be pretty simple to migrate.
And thanks, dan, for your offer. I'll try to get the prototype online soon so you can start kicking its tires.
– raph 24 Dec 2006
Switching database engines is easy with many of the interfaces today. I used Sqlalachemy just now, and it basically works with all the big engines without change to code (my underlying engine was Postgresql).
The important thing is the database schema. And it would be something I would consider early on.
It feels, raph, that you already have the seed of a prototype. So you probably have thought about the schema already. So you can post an initial idea of it. Otherwise it might be wise to think about it "out loud" here.
– dan 25 Dec 2006
To ocat:
Thanks for your feedback. I wasn't in a particularly good mood when I wrote the original, so I've changed that to reflect my true thinking about the differences of vision between the PM'ers and my ideas for Barghest.
There are many approaches to project management, and Ghilbert is about as far away from the traditional waterfall model as I can imagine. That said, I haven't been very actively recruiting collaborators, and in some ways it has not been an especially well managed project. Your example of the lack of spec is particularly on point, and it is about time for that document to come together, now that I have reasonable confidence that I won't be making fundamental changes in the proof language.
--ocat
To dan:
Your "feelings" are quite perceptive. What I have so far is pretty much a very basic wiki, without much Ghilbert-specific functionality yet. I've put it online at barghest.ghilbert.org, and there's a darcs link from there. The next step is to make it to dynamic proof display, something vaguely resembling the Metamath proof explorer. I am encouraged by my experiments so far.
The basic schema so far looks like this:
+-------+--------------+------+-----+---------+----------------+ | Field | Type | Null | Key | Default | Extra | +-------+--------------+------+-----+---------+----------------+ | seqno | bigint(20) | NO | PRI | NULL | auto_increment | | uname | varchar(20) | YES | | NULL | | | what | varchar(255) | YES | | NULL | | | cmd | varchar(20) | YES | | NULL | | | data | mediumblob | YES | | NULL | | | mtime | datetime | YES | | NULL | | +-------+--------------+------+-----+---------+----------------+
The seqno reflects the essential append-only nature of the database. There may be other transitory databases for efficient rendering, but the idea is that those can be regenerated from the log, which is the authoritative source.
The 'what' is the name of the resource. The theorem addcom in the peano module would be identified as something like "pax/peano/addcom". The URL "pax/peano.gh" would resolve as an SQL query that pulled all the records matching "paxpeano*". I know traditional DB technique would be to have lots more entities, representing directories and so on, but my main inspiration here is darcs.
The 'cmd' says what happened for the resource to get its new value. Right now it's just 'u' for update, but things like renames and deletes would also have corresponding cmd values. It's also possible that I'll update the cmd field to implement revoking of commits made in error or in bad faith. Of course, that's not entirely in accordance with the log philosophy, but I think it can work out well enough.
'uname' and 'mtime' are just the username and modification time for the person who made the change. They have little relevance to the semantics of the content, but are present for human consumption. I'm strongly leaning toward an optional log/commit message, as well, along the same lines.
'data' holds the new contents of the resource. For a wiki page, it's just text, and for a proof, it's just the ASCII representation of the s-expressions. I considered representing it as a diff (to be even more darcs-like), but I'm not worrying about disk space, and just storing the whole resource is simpler and more robust (there's never a chance that the patch fails to apply).
– raph 25 Dec 2006
I had an idea that may be helpful, regardless of the granularity of your final database design (ginormous blobs at module level or whatever…) One of the essential attributes of a "database" is that the DBMS can maintain structure by ensuring that the referential integrity of associated table entries is maintained (erroring updates the violate pre-established rules.) This means, for example, that with proper R.I. rules it is not necessary to re-validate the data after it is updated in the database – it is just used afterwards (though double-checks can be written.) So, with a database version of Metamath or Ghilbert it might not be necessary to re-verify all of the proofs over and over again! That would be a tremendous savings, but would require that the cascading effects of changes to a single update entry be properly validated before COMMITing. How to go about this in a free-for-all wiki environment?
I assume that you and your associates will be working on one or more mainline modules that over time will become increasingly complete and perfected. That would seem to mean that updates, accidental or malicious or just plain stupid, would be distinctly unwelcome – just as if Norm allowed me free update access to set.mm, and then had to go back and undo all of my mistakes!
I propose/suggest, instead, defining ownership/update authorities at the module level. That would mean, say, that Raph is Owner of pax/peano. Then, assume User X from Bumduckistan wishes to work on peano theorems. What will he do? He will have his own "supplemental" pax/peano module with only his theorems/proofs in it – and a "D" (devel) status code associated with it. User X's proof verification would then be performed internally against a composite of the "P" (production) status modules + his "D" status pax/peano module. Then, if he desires his theorems/proofs to be merged into the mainline module, he updates a "request" flag on his module – at some point in time, the owner of the "P" status module either accepts or rejects, and the merge operation is performed, along with any additional validation needed as a result of the updates.
A key point here is that rollback of a module's versions is something that is very dangerous for the referential integrity of the database because of inter-module dependencies. So, as a practical matter it is probably best to design the database so that if a rollback is needed it occurs at the database level, and not just one module – or that it occurs only for "D" status modules, upon request by the owner(s).
--ocat (first thoughts, hastily typed…fyi)
Replies to ocat:
On delegating in the free software world. It would be nice if I could play resident genius and have a bevy of assistants who would take my specifications and produce implementations, but I'm unaware of any succesful project in the free software universe which works that way. Every viable project I know about started with the designer writing some code.
But there are successes based on good, clean interfaces between modules. One of my favorite examples is the plug-in system for Gimp, which was an easy way to get one's feet wet in that project. The Unix philosophy basically works the same way: each tool does one thing well, and then it's possible to string them together to do more complex things.
The most basic such interface is the Ghilbert proof language. It's taken a while for me to gain confidence in its suitability, but (after a bit of incremental improvement) I now believe it is. In my vision of a Ghilbert ecosystem, there would be many tools, translators, browsers, provers, etc., that read and write this proof format. In my opinion, the simplicity of the proof language is the most important qualification for its lingua franca status in such an ecosystem.
Another such interface will be the ability to retrieve theorems from and post theorems to ghilbert.org. This interface will make such things as automated theorem proving bots possible. A user posts a proof goal, the bot retrieves it, and, if it finds a proof, posts that. One thing I find particularly appealing about this model is that these bots can be quite diverse. One, for example, may only know how to do symbolic algebra, while another does general brute-force searching of the proof space. Further, these tools can be written in any language, have dependencies on other huge systems, or whatever.
It certainly is important for these interfaces to be well documented, and I'll make that a priority. Thanks for reminding me.
Lastly, why should I G.A.S.? Well, largely because I think I can do a good job building the basic tools myself. I actually have considerable experience implementing web content management systems, and certainly a strong intellectual curiosity about how to do it Right.
On granularity. The granularity I proposed above is theorem-level. Module-level would be too coarse for a variety of reasons.
On the unification algorithm. A proof assistant needn't concern itself with definitions and expansions. Almost all of the time, the definition expansion mechanism in Ghilbert is used only in the theorem that proves the definition - in other words, what would be the $a statement in Metamath. These definitional theorems are, in turn, almost always trivial (alpha-conversions at worst, typically), and will probably be largely automatically generated. Once the definitional theorems are in place, you just use them as you would any other theorems, without having to worry about whether the term was defined through a def command or in some other way.
On scalability. It's worth worrying about scalability, but my gut feeling is that we have a couple of orders of magnitude of headroom before hitting any serious limits, just doing things the simplest way. set.mm is now almost 10k theorems, and is about 5MB uncompressed. Scale that up by two orders of magnitude, and you still have something that can easily fit in RAM on the server. Further, Shullivan should be able to verify an entire database of this size in about a minute, projecting from its current performance (500ms for set.mm).
But a 1M theorem database is not practical as a single huge chunk like set.mm. That's one of the motivations for Ghilbert's module system. When working on a specific theorem in a particular area, you'll just import the modules you need. Further, I wouldn't be surprised if a significant fraction of the theorems in the database turn out to be for support of automated provers (assump.gh has this flavor, even though I've been extensively using it for manual proving).
So, I think, most tools will only have to deal will with a working set comparable in size to the existing set.mm, for which doing things the simplest way is a perfectly fine solution.
On version control. Two people hit the "edit this page" button on the wiki at about the same time, get the text downloaded into their client, do their edits, then hit "save" or "commit" or whatever. Now you've got a concurrency problem. What do you do about it?
In particular, at what level can you solve this problem? Transactions and concurrency control at the database level won't help at all. The approximate mapping of techniques from that world is to implement an exclusive write lock, so you say "I'm going to edit this file," then nobody else can acquire the lock until that transaction is committed or aborted. However, that model is unpalatable (I remember using RCS in a four-person office in this way, and finding it annoying even at that scale), and the web has moved beyond it.
As I mentioned above, one of the inspirations I'm drawing on is darcs, which addresses these problems in a simple and clever way. In darcs, a repository is a log (linear sequence) of diffs. You can reconstruct the current working state by running all the diffs in sequence.
If two people generate two different repositories (it's a distributed system, after all), then the basic version control operation is to merge the diffs that differ. At heart, what it does is very similar to a three way merge, but it's actually doing what it calls "patch commutation" under the hood. In happy cases, it's able to reconcile the two sets of patches automatically, but, as with all revision control systems, sometimes it just can't. In those cases, manual fixup is needed to actually get a merged repository.
If I wanted to support this tree-like structure in Barghest, then basically I'd need to add a "based on" field (list of seqnos) to each log commit. Then, both new revisions would go into the database, perhaps under user-local namespaces, and a merge would conceptually be a separate operation that would create a new revision "based on" the seqnos of the two that were merged.
But I'm really not sure I need this level of sophistication (and attendant complexity). What I'm far more inclined to do in this case is present a choice to the user who clicks "commit" the second time: commit the new version, smashing the other set; abandon the new version, keeping the other set; or do an explicit merge, perhaps starting with the best attempt to do an automated three-way merge.
On integrity. Ghilbert is something of a unique case in that integrity of proofs is well defined and mechanically verifiable. (Discussions and so on are less so, but let's focus on proofs here). Once a theorem is proved, it really can't be un-proved. There will be cases of definitions changing and the like (such as Norm's change of sum notation around 12-Jan-2006), so version skew isn't totally banished, but still, at a conceptual level, a valid proof is more or less immutable.
Ghilbert will only commit proofs to the database when they are valid with respect to the rest of the database. Thus, if you pull a snapshot of the database from when the proof was committed, it will always verify. (Note that the log approach makes it quite straightforward to pull a snapshot, you just add a "WHERE seqno < whatever" clause to the SQL).
Of course, changes to the database may cause theorems to stop verifying. This may be for several reasons, including vandalism, simple renaming of theorems, or deeper change of notation as above. I have several ideas of how to deal with these cases.
Note that I've described a bunch of these operations in terms of rolling the logs of the entire database. By also storing a dependency graph (which can be derived from the log), it should be possible to do most of these operations incrementally. But, at first, I'll do things the simple way, and then I have the advantage that the simple way serves as something of a spec for how the more sophisticated approaches should behave. Also, I'd love to have the problem of a database so large that a linear scan through it is impractical, for that means that the project will have succeeded wildly.
– raph 26 Dec 2006
raph, after first applauding your work and thanking you for making it public (and the code looks really clean too (what kind of a complex sentence is this, anyway? :-) )), a quick question: How will 'interface files' (.ghi files) fit in to Barghest? – marnix 28 Dec 2006
Thanks, marnix!
I'm still playing with the way that the database holds Ghilbert statements and proofs. My current thinking is like this:
The names of objects in the database form (conceptually) a hierarchical directory structure. I've already started down this road with entries like user/marnix. I'm thinking now that a theorem is not a leaf node, but rather a directory that contains (optionally) several different types of leaves:
The first two of these are s-expressions, the second two are markup. This list is intended to be somewhat open-ended, and it's fun to think about other things that might go in there.
Then, a .gh or .ghi file in the database also has some content, which is primarily a list of thm's or stmt's, respectively. This would also include other interfaces imported, declarations of variables, kinds, and types, and perhaps other things. I'm thinking of making this file just like a .gh or .ghi now, except that the argument to thm, stmt, or def is just the name of the symbol defined.
So, pax/peano/peano-thms/.ghi would look something like this:
param (PROP pax/prop () "") param (PRED pax/pred (PROP) "") param (PEANO pax/peano (PROP PRED) "") var ( wff ph ps ch th ta ) var ( val A B C D A' B' C' ) var ( var x y z x' ) stmt addcom stmt mulcom ...
And pax/peano/peano-thms/.gh would look something like this:
import (PROP pax/prop () "") import (PRED pax/pred (PROP) "") import (PEANO pax/peano (PROP PRED) "") import (PROP-FULL pax/prop-full (PROP) "") import (PRED-THMS pax/pred-thms (PROP PRED) "") thm addcom thm mulcom ... export (PEANO-THMS pax/peano-thms (PROP PRED PEANO) "")
By quick test, these files are about 90k each for the translated set.mm, so they're quite reasonable to take in one gulp.
Reconstructing actual .gh and .ghi files would be fairly straightforward - you'd just pull a record out of the database for each arg that's not a list. You can also include more or less in the way of text (each line prepended with "# ") depending on what it's going to be used for.
– raph 28 Dec 2006
Hi Raph,
I think that connecting a wiki with a proof checker is a good idea. My opinion is that it could be used to have a proof and nicely typeset comments on the same page. Maybe you could use some literate programming techniques to hide the less important part of the proof (maybe !). But in fact I see two problems. By working with Metamath I realize that a theorem doesn't exist in itself. It only exists according to a goal. For instance in set.mm we could add many variations of the same theorems. But Norm carefully chooses the theorem in order that the database doesn't explode. It's what I'm afraid with Barghest: if there is no goal your project could go nowhere. The second point I would like to tell about is the format of the database. Ghilbert has its own database format, Metamath has its own and Mmj2 has its own as well. Since the data are always the way many projects can be connected together I think there is a potential future problem if a total connectivity is not ensured between Metamath, Barghest, Ghilbert and Mmj2 (and others). – fl 29-Dec-2006
fl – You're quite right to be concerned about connectivity. There are two basic approaches to this: define the One True Format for Everything, or have different formats adapted to different needs, and make sure it's easy to translate between them. I'm solidly in the latter camp, and you can see that ocat has taken a simlar stance with the Proof Worksheet format.
There's already a mm_xlat.py in the Ghilbert darcs repository which converts Metamath to Ghilbert (and I'm making it convert the comments to Barghest markup as well), and I have a (not yet released) to-mm.py script which converts Ghilbert to Metamath. That's how theorems such as cnsscnp got there.
Even with the idea of a translator, there are still things that can be done to reduce "impedance mismatch" between the various systems. To this end, I've suggested to Norm that he adopt Barghest-like markup as the standard for text within Metamath files, and have offered to create a patch for this. If he accepts, then at least text can flow back and forth freely without having to go through (much) conversion.
I have a really simple idea for representing abridged proofs: in the proof source, you simply separate the important parts by blank lines. The abridged view shows only the result (or perhaps the last line) of this block, with a "+" icon like a tree view. Click that, and it expands to show all the steps. Voila, stretchtext for proofs. I've been using this technique to structure proofs in places like pax/pred-thms.gh, and I find that it helps readability a lot. See iotabaz, for example, which is divided into five blocks of two to six lines each (average 4.5).
– raph 29-Dec-2006
Hi O`Cat and Raph.
On connectivity since I often use Mmj2 I will use it to show how different formats can lead to difficulties. When you are working on a proof you simply use eimmexp.cmd and eimmimp.cmd to transfer it from Mmj2 to Metamath and back. It is a bit long but it's not really important. The very problem is that the Proof Worksheet format and the mm format doesn't fit together. Suppose for instance that I have begun my proof in Mmj2. I have a d statement, some comments and different scraps of proof that are not connected together. If I want to export this proof to Metamath I must remove the d statements and the comments otherwise eimmimp.cmd doesn't work. Once I am in Metamath the non connected scraps will be linked by dummylinks. Then I work on this proof in Metamath and I translate it back to mmj2. It means that now the proof has no d statement and no comments any longer and that the non-connected statements are now connected with dummy links. Not exactly the same proof as you can guess. The consequence is simple I don't use d statements, nor comments, nor unconnected scraps of proof because I know that I won't be able to export my proof. And to export my proof I need ! On the other hand d statements, comments and unconnected scraps of proof are in my opinion very important features of Mmj2. I wonder if there is not a way to allow to use these features and to ensure that Mmj2 and Metamath are completely connectable. Suppose that a window in Mmj2 contains the main proof. In this window there is no d statement, no comment and there is only one scrap of proof. This way Mmj2 and Metamath are perfectly connectable. In other windows I have added some comments, a d statement and I've tested other unconnected scraps of code. Since they are not in the way of the main proof they can't alter the connection between Metamath and Mmj2. And since we use the extra features of Mmj2 it means O'Cat's intent is respected. – fl 30-Dec-2006
I had a look at Ghestalt. It is very beautiful and simple. Raph (and Dan) seems to be the specialist of the interesting softwares in less than 600 lines (since it was the record he had won with Ghilbert ). The idea of adding a wiki to a proof checker still seems to me really interesting. I think however that the proofs are not human readable. I wonder if it would be possible to store the proof and to hide it and to print a more readable stuff just like in the Metamath proof explorer or in mmj2. – fl
Thanks for the visit, fl. That is indeed the idea. I'm a little hung up on trying to design/choose the best markup language right now, but the idea is very much to store the proof as S-expressions, and display it much like the Ghilbert interactive app, but probaby with the proof lines and proof stack more finely interleaved.
There are a number of modest technical challenges to be overcome. One is to extract the relevant bits of proof context from the database on demand, rather than doing batch processing of the entire .gh file. Another is how to get nicely typeset math to show up in a lowest-common-denominator browser. My choices, roughly in order of decreasing preference, include:
I'll put something up fairly soon, and hopefully, before too long, it will actually become a useful tool.
– raph 2007-01-10