search

UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 23 forks source link

automate JEdit plugin update #370

Open kohlhase opened 6 years ago

kohlhase commented 6 years ago

When we make a new MMT release, then we have to update the MMT plugin for JEdit (a somewhat un-necessarily tedious process) that is easily forgotten (see for instance in the KRMT course https://fsi.cs.fau.de/forum/thread/16235-MMT-update). And then nothing typechecks in JEdit, leading to uncertainty and frustration of users.

We should think about a design of the plugin and/or the MMT release distribution mechanism that makes sure that the JEdit plugin update actually happens and is as painless as possible.

And while we are at it, we should think about how to get plugin updates painless after pulls on devel (think about the developers as well).

Jazzpirate commented 6 years ago

I agree that it's easily forgotten, but I really don't see how to make it more convenient than the single terminal command it is now...

kohlhase commented 6 years ago

... than the single terminal command it is now...

actually two comands (from memory) ... uninstall followed by ... install that can be combined.

Jazzpirate commented 6 years ago

... install will do. uninstall you really only need if you want to make absolutely sure that even the user-adpted files (abbreviations etc.) are completely reset. For the students install is enough :)

kohlhase commented 6 years ago

Maybe the JEdit plugin can "remember its own version", and check it against the "MMT version" and warn (with instructions) if they differ.

For the developers one could do the same with "GIT revision" or "GIT date".

kohlhase commented 6 years ago

then we should have a reset that does both, that sounds more convenient to me.

Jazzpirate commented 6 years ago

The confusion here is that there is no difference between "the jEdit Plugin" and "the MMT version". There's (basically) an mmt.jar in the jEdit-config-folder and it has no canonical other thing to compare its version to. I think that's the main source of confusion: The conception that "THE mmt" is the jar-file in the deploy folder and replacing it will do... well, anything; whereas the jar-file should probably be better thought of as a setup file only, that needs executing before anything will be updated.

kohlhase commented 6 years ago

Thanks for reminding me (I had not remembered)

Then (to quote @florian-rabe) "this is terrible design and must be eliminated".

We really need to get rid of this "two jars design". Maybe symbolic links help or just a reference to the JAR in JEdit?

kohlhase commented 6 years ago

One way out of this would be to distribute JEdit with MMT like the Isabelle people do.

lambdaTotoro commented 6 years ago

Another could be to only use some canonical MMT instance for the plugin, instead of its own. We would have to make clear to the plugin where that instance is, though (file system links, environment variables, config files, ...?).

florian-rabe commented 6 years ago

jEdit reads the mmt.jar from a specific folder, into which the mmt.jar must be copied. The mmt.jar in the deploy folder is never used by jEdit.

Symbolic links would be OS-specific and thus more complicated. Note that this is not necessarily desirable anyway - for example, I only copy over a new mmt.jar once it works.

To copy over the jar, the above-mentioned install command can be used. Building-from-sources users additionally have the option to run the sbt target jedit/install.

To make this more convenient for download-jar-and-use-jEdit-only users, we could add an update button inside jEdit that downloads the latest mmt.jar. Caveat: Some fiddling might be needed to overwrite the jar while jEdit has opened it; this used to work, but recently I've had difficulties on Windows. Ideally, this would happen via the jEdit plugin manager, but I found the workflow for getting mmt.jar onto the jEdit servers too complicated.

Jonas's suggestion would also work, but would be more complicated.

florian-rabe commented 6 years ago

The update could also pull all relevant archives which are released at the same time.