Is set.mm available in a more "machine-readable" format other than in html?

[Humanities Clinic]

Is set.mm available in a more "machine-readable" format other than in html? For example, in json, or sql, or mayb in a graph database file like neo4j?

[Mario Carneiro]

MM is already a "machine-readable" format, it is not much harder to parse than JSON (depending on what kind of information you are interested in), and you can even reasonably parse it with regexes, especially if you stick to MM files with a standard layout like set.mm. Your query about graph file formats suggest that you are interested in theorem references? If so, you can get this information fairly easily from a regex, if you search for a label followed by $p, some stuff, $=, and then a list of theorem references inside parentheses.

On Mon, May 29, 2023 at 1:03 PM Humanities Clinic <humaniti...@gmail.com> wrote:

Is set.mm available in a more "machine-readable" format other than in html? For example, in json, or sql, or mayb in a graph database file like neo4j?

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9ef3a9e5-2510-4deb-9f17-6ab25ad533b5n%40googlegroups.com.

[Jim Kingdon]

My mind went to metamath-exe commands like SHOW USAGE and SHOW TRACE_BACK and even SHOW PROOF. Agreed that the question will depend on what one is trying to find out, but parsing the HTML is probably more difficult than other approaches (at least for most information you'd want - there might be exceptions).

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvQt6D6xoufTE5%2BbvyKmfUVN0R0AZK0Ch_7qfLbR95Duw%40mail.gmail.com.