> FYI: I tried loading the page, I get "Loaded N" where N rapidly > counts up to 42869 and then nothing happens. This happens even after > a reload, set.txt is cached so that doesn't seem to be the issue.
Yup. The text above the loading count gives you the keyboard shortcuts for doing anything. I know it's a terribly undiscoverable UI at the moment. The description wasn't there until an hour or two ago when I added that so it would meet the bare minimum of sharability. Anyway, if the description doesn't help, just press the forward slash key, and a fuzzy-finder window should pop up that you can search through all the assertion labels that have been loaded. > This kind of approach is fine for toy projects but for 'real' > projects that you want to be used by the community this is > not-invented-here syndrome. Even if you don't want to write rust > code, one thing you can do is document your implementation strategy > and feature set so that the code can be ported by others. I agree that it's a good idea to document the interesting parts of the project so that other efforts can benefit as well. Some of my motivation is intentionally NIH, since making things helps me learn how they work and I also find using libraries that I've written more fun than using libraries other people have written. I disagree that building a new library when one already exists is always bad idea; if you don't think that either, than maybe we only disagree on the criteria of when to do it. Anyway, that's a much larger debate that doesn't need to be settled here. I'm just answering the original question of why I would work on a new project instead of contributing to an existing one. Maybe worth mentioning is that I haven't built *everything* from scratch. I'm using a lot of existing OCaml libraries that I'm not that interested in building myself (or else I already have and concluded that my version was worse than the existing one). > I think this opinion is formed from an incorrect guess of how things > are done in mm-knife, if you are talking about that. Verifiers are > generally written as you say, but proof assistants have to have a > more incremental view of things, and mm-knife is the only proof > assistant that actually has incrementality built in (even mmj2 and > MM-PA don't really support incremental updates). Interesting, sounds like I'm mistaken. The incrementality I'm taking about is pretty pervasive. If you can figure out how the demo I linked works, then you'll be able to step forward and backward through proofs and see the stack and heap growing and shrinking as the steps are executed. The stack and heap are represented with immutable maps that share most of their structure between each step so that you can you step forward with minimal recomputation of the virtual-dom tree; that is, you only need to compute the newly added items to the stack, instead of recomputing the whole page again. Does mm-knife have incrementality during the execution of a single proof? I could be wrong, but my approach sounds like it would not achieve the lightning speeds that I've heard mm-knife is capable of. In contrast, my verifier takes about 13 seconds to verify set.mm. There's an argument to be made that virtual-dom + persistent data structures + all these other incrementality abstractions + js_of_ocaml's slow compilation scheme are making my program more complicated and slow. Maybe if I were to just do DOM manipulations it would be faster and less code. Maybe, but I'm skeptical, and I also don't think I would enjoy working on it as much, and I would probably write more bugs. > If you are compiling to web assembly, I don't think the system support > really matters, you are ultimately constrained by the browser in the > end. Besides, I don't think target support is an issue these days no > matter what language you choose. > > Interestingly, if you are using web assembly (EDIT: or compiling to > javascript, if the *.bc.js files are any indication), you might not > even need to link them together directly, since they can both just > separately talk to javascript. Yeah, that's right. I'm using js_of_ocaml, which translates the bytecode output of the ocaml compiler into javascript. I'm sure you're right that it could be done. I would still contend that having bindings is inconvenient because you have to think about how your language's runtime will think about different pieces of data. Like, you probably can't define a variant type in Rust and have it be translated to a variant type in OCaml (unless you write that marshalling code yourself). > There is a big difference between proof of concept and production > tool. I *strongly* recommend centralizing efforts for the latter, and > while it's fine to do the former in any language / project, I think > that it is easy to start dreaming bigger and planning for more users, > adding more features, and sinking a ton of time into something that > ultimately leads to fragmentation. I agree with this, mostly. I think what I am saying is that proof of concepts are a fine reason for fragmentation, and then at some point a "rebalance" operation should happen where the ideas get put into one tool. Obviously it's great if those ideas get put into the same tool from the beginning, but I could also see that slowing down projects where the author wants more freedom to experiment than the project provides. > Metamath *verifiers* are easy to write, but metamath *proof > assistants* not so much. I think the need for centralizing our fairly > small pool of manpower is because the proof assistant-styled features > are not nearly powerful enough in any system except to some extent > mmj2 and MM-PA, both of which are severely hampered by losing their > principal architect / maintainer. Fair point, although all the "fracturing" that's been mentioned seems to be about the proliferation of verifiers, and not proof assistants. My experiment is currently just in the direction of an interface for visualization and exploration, which I *think* is orthogonal to building a proof assistant? I do eventually want to build a proof assistant into this, though. > Rust vs. OCaml As fun as language wars are...no need. - Philip -- 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/20220531195336.0f47c87b%40ithilien.
