I was thinking of the latter: have two crates, one for the library and one for the executable, and put assorted functionality in the command line tool and keep the library focused to things that make it easy to write the CLI and are metamath-related.
On Thu, Jun 8, 2023 at 7:24 PM Thierry Arnoux <thierry.arn...@gmx.net> wrote: > 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 <dwhee...@dwheeler.com> > wrote: > >> >> >> > On Jun 5, 2023, at 8:48 AM, Thierry Arnoux <thierry.arn...@gmx.net> >> 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 --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 metamath+unsubscr...@googlegroups.com. >> 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 metamath+unsubscr...@googlegroups.com. > 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSszF2krw69MRt4Fbg1FqngSGeOFGNpSR3%2BiC%2BJWJedkZA%40mail.gmail.com.
