Splitting crates

[tirix]

I'm opening this issue to discuss the details of splitting metamath-knife into a binary and a library crate, namely naming and directory structure.

I think what makes more sense is to keep metamath-knife for the binary, because this is where a lot of functionality will land (thus the "swiss-army" knife metaphor). We could maybe name the library metamath-rs, with an ending in -rs like for many other rust libraries, knowing that this is the only Rust library I know of for Metamath (I'm not counting Stefan's original smetamath-rs, of which this is a fork).

As for directory structure, we could simply follow the workspace model and have two directories below the repositories root.

@david-a-wheeler @digama0 what do you think?

[david-a-wheeler]

The basic idea makes sense to me. Certainly splitting up "front end" from "library" makes sense. I would assume a lot of the functionality would end up in the library though. I would expect cli ui to end up in the front, and the work to compute and return things to be in the library (ready to use by a cli tool, gui tool, server, whatever). So maybe we're thinking differently about the boundary?

[tirix]

Right, we should also discuss the boundary!

I think the idea of the split was triggered by the "graph export" functionality I recently added, so that function would also go into the binary, beyond handling command line and displaying output.

I think the library should include functions to:

• read and parse the database in MM format (in),
• write the database in MM format (not yet in),
• verify proofs, formatting, definitions, etc (mostly in).
• handle proofs : build or extract a proof, traverse it, update it (in, except for update),
• handle formulas : build or extract a formula, traverse it, update it (in),
• handle statements : build or extract a statement, update it, (not yet in)
• handle other MM data (chapters, typesetting, commands etc.)

What's not in scope of the library would be:

• human readable output : GUI, Web, or text output (except for MM file format),
• proof assistant, i.e. suggesting or finding a proof for a given statement,
• exporting all kinds of statistics or graph from a database. The library only provides access to the raw data, further treatment is out.

I'm unsure about functions like "axiom usage", "discouraged" and "minimize", but I tend to think they should be part of the library - or maybe an extended library crate?

[david-a-wheeler]

That makes sense. I'd put a little more in the library:

exporting all kinds of statistics or graph from a database. The library only provides access to the raw data, further treatment is out.

The library shouldn't have graphs, as that is I/O. But I think some basic stats and the api to walk the data could be in scope.

I'm unsure about functions like "axiom usage", "discouraged" and "minimize", but I tend to think they should be part of the library - or maybe an extended library crate?

I think those make sense to be in a library. The idea if splitting the library into "basics" and "extensions" is intellectually appealing. Do we anticipate anyone using then this way?

[tirix]

The idea if splitting the library into "basics" and "extensions" is intellectually appealing. Do we anticipate anyone using then this way?

I can imagine that in some cases you want the smallest possible footprint for your application, either because you want to launch it on a mobile device, or maybe over the web, compiled using WASM (which is possible with Rust). In those cases it would be interesting to have the simplest possible library, with as few dependencies as possible.