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).
On 5/29/23 10:08, Mario Carneiro wrote:
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
<http://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
<[email protected]> wrote:
Is set.mm <http://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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/9ef3a9e5-2510-4deb-9f17-6ab25ad533b5n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/9ef3a9e5-2510-4deb-9f17-6ab25ad533b5n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSvQt6D6xoufTE5%2BbvyKmfUVN0R0AZK0Ch_7qfLbR95Duw%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CAFXXJSvQt6D6xoufTE5%2BbvyKmfUVN0R0AZK0Ch_7qfLbR95Duw%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/cb309b99-548e-2373-21c8-a5ec86277447%40panix.com.
