> 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/20220601174227.09788370%40ithilien.
