Nice discussion. Three things I wanted to contribute if they're at all useful:
1. If anyone needs beta testing on a system then I'd be happy to play around with it and give, rather non-expert, feedback. I tried your system a little Philip, it was really cool to be able to see the stack and heap while the proof was in progress, that's new to me which is nice. 2. At some point I'd like to make a mini course for getting people into metamath, a few videos of explanation with some worksheets of problems to try to help newcomers find their way. Maybe when mm-knife has a VSCode extension would be a nice time to do this. I think making it smoother to get into the community can help with growth. 3. I used to work on an open source game called Thrive. We would put up posts (for free on places like reddit) showing off the game and asking if anyone wanted to contribute (again for free, as open source) and we would get a reasonable number of people. Is it worth appealing to Rust programmers, for example, who might not know so much about the metamath side but might be keen to help and be able to work on UI, web stuff, cross compatibility etc? If that's helpful I don't mind doing the legwork of writing the posts and finding appropriate places to put them (you have to be sensitive to subreddit posting rules etc). On Wednesday, June 1, 2022 at 10:32:18 PM UTC+1 Philip White wrote: > > Thanks, I got the basic functionality working. A few more bug > > reports: I haven't been able to figure out any conditions under which > > the (shift-)hjkl buttons do anything; and the fuzzy finder does not > > prioritize exact matches which makes it difficult to jump to specific > > theorems. > > You have to add more than one assertion to the workspace before any of > the window manipulation commands do anything. This is because the > windows are arranged in a row of columns, and not in arbitrary > positions determined by the user. h and l move back forth through the > columns, and j and k move up and down in a particular column. > > Prioritizing exact match is a good idea. The current sort is > alphabetical, but it would be great to use the actual FZF algorithm. I > also would like to add more information to the search box so that the > user doesn't just have to search through the mnemonics, which are to > brief to know what something is before selecting it. It would be nice to > search for "Axiom of Choice" and have the system show "ax-ac" at the > top. Maybe this could be accomplished by including the first sentence > of the attached comment? > > > Regarding incrementality during execution of a single proof, that's > > up to you. The way you step through a proof is actually > > user-(of-library)-configurable, and I would generally expect a UI to > > implement its own data structures which support the required stepping > > operations without moving a lot of data. > > Oh, that's quite interesting. I suppose I should actually look at the > mm-knife API at some point. > > > Personally, I wouldn't try to do this with a UI framework at all. > > General purpose virtual-dom diffing is just objectively worse from a > > performance standpoint. I would just have stepping send change events > > that push and pop things from the stack and/or heap. (But also, this > > is not at all the bottleneck - you can do pretty much anything you > > want in this space and your debugger will be performant enough.) > > The virtual-dom approach is slower than doing direct DOM manipulation > of the exact things that need to be changed, but I think it clearly > wins if you want to take the "compute your view with a pure function" > approach, since it will minimize the number of DOM mutations. That is, > I like the "view is a pure function" approach because it is pleasant > and seems to yield fewer bugs, so I also use a virtual-dom library > because it makes that approach feasible. > > > Actually you can: I haven't used the 'ocaml' rust crate but it seems > > to have some pretty great support for marshalling complex types, > > including variant types: > > > https://docs.rs/ocaml-interop/0.8.8/ocaml_interop/macro.impl_to_ocaml_variant.html > > . The usual way would be to put a #[derive(FromValue, ToValue)] > > attribute on the type definition, like shown in the first example > > here: https://docs.rs/ocaml/latest/ocaml/index.html . > > > > If the communication was indirect via webassembly it probably > > wouldn't be as nice as this though, since you would have to marshal > > your types into JS and from there to rust (so it would be using a > > WASM <-> Rust bindgen instead). Still, you could probably encode > > variant types to JSON and get essentially fully automatic FFI for > > complex types, as long as both ends have the same conventions for > > encoding (and I know the rust deserializer is configurable to other > > conventions even then). > > That's pretty cool. > > To elaborate a bit on the "Rust is too low-level for me" comment: what > I mean is that there is some syntactic overhead related to memory > management. My impression of Rust is driven by using it, actually; I > don't hate it, and I would 100% use it instead of C or C++. I'm aware > of some of the things that Rust has to make manual memory management > less error-prone and more convenient, but it doesn't make those > concerns go as close to zero as a GC. > -- 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/2d628826-c279-455c-ac87-ed965a2e18b2n%40googlegroups.com.
