Hi Mingli, The embedded Javascript engine is used to run auto-transformations, that is a function I find quite indispensable. Might a different branch for before/after JDK 15 be a solution?
With the EMetamath Eclipse Plug-in, I have reused the core of MMJ2, without reusing its GUI. With Rust and metamath-knife, we try to have this kind of modular approach: metamath-knife <https://github.com/david-a-wheeler/metamath-knife/issues/64> is meant as a toolkit library which provides database parsing, verification and access, and we can built several tools using it, like command line tools, web pages generators, proofs assistants, etc. BR, _ Thierry On 14/02/2022 13:49, Mingli Yuan wrote:
Hi, Thierry, There is a tiny fix worth sharing, I am thinking about how to fix it on the official repository and issue a PR. The nashorn javascript engine was removed from JDK 15, in order to make macro work, we have to add nashorn back, this may involve several tiny changes. With only the Ant build system, adding nashorn might be a little bit cumbersome; also the official repository needs to support multiple JDK versions.... As mentioned by Eric Steven Raymond in his /The Art of UNIX Programming,/ there are two styles of application design: - monolithic design - composability by small toolkit The jpackage tool bundles the jar and JRE together, the final deliverables can eliminate multiple Java environments. But it is a monolithic way, the parser, the verifier and others, by nature, are small composable toolkits, and are userful by themselves. That is why I don't think monolithic gui is the right solution. Mingli On Mon, Feb 14, 2022 at 12:46 PM Thierry Arnoux <[email protected]> wrote: Hi Mingli, I have not tried your MMJ2 package but if it includes the correct Java version, then it might be the right solution (MMJ2 only supports Java 8, if I understood well). Would there be a way to provide binary versions so that users would not have to build it themselves from source? I see you have included MMJ2's sources in your repository. If you have done any modification worth sharing, please consider also a PR to the official repository! (https://github.com/digama0/mmj2) BR, _ Thierry On 14/02/2022 11:24, Mingli Yuan wrote:updated: mmj2 has tests on windows, but not on linux and pure junit based cases. On Mon, Feb 14, 2022 at 10:22 AM Mingli Yuan <[email protected]> wrote: Hi, folks, I had read the long discussion history about mmj2 installation on github: - https://github.com/digama0/mmj2/issues/14 - https://github.com/digama0/mmj2/issues/21 - https://github.com/digama0/mmj2/issues/36 - https://github.com/digama0/mmj2/issues/37 - https://github.com/digama0/mmj2/issues/39 Lots of the questions had already been solved, some still haunted there. Especially in Issue #39, @digama0, @david_a_wheeler and @cwitty discussed the problems and the engineering complexity for future fixes. After considering all the above in an hour, I don't think the installer in my previous mail is a good solution, it is only one possible option. I respect all the contributors' works and understand the status of open source development. We had already improved a lot, but still did not achieve the goal For me, there are two sets of engineering problems beneath domain problems, maybe it is biased on my preference and experience. 1. homework: - 1.1 the build system: ant is OK, nowaday developers use gradle and others, the tool chain of Java evolved a lot. - 1.2 lack of test cases stops people outside to contribute further. 2. application problems and solutions - 2.1 multiple OS support: at least Windows/Linux/MacOS - 2.2 multiple Java environment support: Java 8 and aftermath, esp. the LTS versions - 2.3 a well-designed convention and workflow on metamath/mmj2 develop: where do we put the database and personal works, etc. Above these pure engineering problems, it is the problems of metamath and math, the beneath and above two parts are orthogonal. It means a developer can focus on engineering problems without introducing too many domain problems. As any open source projects, the engagement, trust and time are real problems. I used to be a Java developer for years and I can contribute some. I also propose a way to solve these: - migrate the build system to a new generation builder - give sanity tests on set.mm <http://set.mm> and other databases - give more test cases on basic functionals - once tests are ready, we can integrate a CI to check on different OS and JVM By this way, we can define our engineering problems very clearly, all the problems are surfaced on one page with different status on different platforms, and then we can fix them one by one. @digama0, @david_a_wheeler and @cwitt, what do you think about the proposal? Mingli On Sun, Feb 13, 2022 at 5:08 AM Mingli Yuan <[email protected]> wrote: Hi, folks, After 1 day of investigation and 1 day of work, I set up a demo repo which can generate installers to ease mmj2 installation. So far only the Mac version *.dmg was tested. The demo upgraded to a higher JDK version, and then generated installers by jpackage which was shipped by JDK after version 14. The main point is - JRE was bundled with the installer together to ease Java installations - use hidden user directories to store default settings and read only database to eliminate initial configurations - Runnable after installation without any configurations Since it is a quick hack and demo, the code was a little bit dirty. If you think it is helpful, I will put more energy on it. Comments and ideas are welcome. https://github.com/mountain/mmj2e Mingli -- 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/CAGDRuAii%3DpexaKG_3t5LX8PEsnkMxhOkxOm3VzFWaDXJZm6Lvg%40mail.gmail.com <https://groups.google.com/d/msgid/metamath/CAGDRuAii%3DpexaKG_3t5LX8PEsnkMxhOkxOm3VzFWaDXJZm6Lvg%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/ee867b54-36f9-348a-ee95-181c03a3f20c%40gmx.net.
