Yes this feature is quite far away from a core functionality.
The `metamath-knife` crate is actually both the library and a command-line tool. What do you have in mind here? - still keeping both library and command-line together, but moving some functionality (like graph exports) to another command-line crate, - or splitting library and command-line tool, with the graph export functionality moving to the command-line tool part? _ Thierry On 08/06/2023 19:40, Mario Carneiro wrote:
I am actually a bit concerned at the growth in behaviors of what is ostensibly a library. We need better separation between the proof assistant and the library, possibly a second crate in the same repo. On Thu, Jun 8, 2023 at 9:48 AM David A. Wheeler <[email protected]> wrote: > On Jun 5, 2023, at 8:48 AM, Thierry Arnoux <[email protected]> wrote: > > Yes, the PR has not been merged in yet, so until then you will need check my branch out. > > This feature required an "XML" library and I've kept it optional, so you will only be able to access it if the program is compiled with the "xml" feature, like so: > > cargo run --features xml -- ../set.mm/set.mm <http://set.mm/set.mm> --time --export-graphml-deps deps.graphml > > Or > > cargo build --features xml I appreciate making it optional. Can you make it so the *default* is to include it, and then optionally exclude it? That way, people can use options to build it for special purposes, but the "out of the box" functionality has whatever people might like? --- David A. Wheeler -- 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] <mailto:metamath%[email protected]>. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/03E6D2BE-FC76-4663-A563-9BE08D9DF2A1%40dwheeler.com. -- 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/CAFXXJSu4TttF50YBYg%3D1x5vwKde6vUcTm1BFLDb%3D_RUU0pxshA%40mail.gmail.com <https://groups.google.com/d/msgid/metamath/CAFXXJSu4TttF50YBYg%3D1x5vwKde6vUcTm1BFLDb%3D_RUU0pxshA%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/5ae70126-861b-2813-8868-9e548d782443%40gmx.net.
