search

UniFormal / MMT

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

Tests missing XZ dependency #392

Closed tkw1536 closed 5 years ago

tkw1536 commented 6 years ago

The tests are failing ever since the XZ dependency was added via unmanaged jars. See e.g.:

https://travis-ci.org/UniFormal/MMT/jobs/429959894#L3394-L3417

This should be fixed.

tkw1536 commented 5 years ago

@florian-rabe you wanted issues. This problem is still the case.

florian-rabe commented 5 years ago

You can add dependencies for the test if necessary.

But I want unmanaged jars for the other targets.

tkw1536 commented 5 years ago

If it was as simple as "adding dependencies", this would be a non-issue (and I probably would have committed something already). I do not know why, but the problem is that in the current setup, the unmanaged jars are treated differently in different targets. The targets I am talking about here are "local setup" and "travis tests".

Suppose we leave XZ as an unmanaged jar in the local target, but also add it as an sbt level dependency for the test target. This will cause conflicts, as we will suddenly use two different versions of a single library in a project. (I have tried this; and in my experience such a thing just leads to more trouble rather than less).

I believe that switching to managed dependencies would make this difference between the environments go away. Additionally, it would give the following advantages:

Of course there are dependencies that do not exist on sbt. As far as I know, these are:

We should (and of course also need to) keep these as unmanaged jars; mostly because they do not exist anywhere else and also they do not cause the problem as above.

I hope this clarifies the situation -- and what exactly the problem is. Can you perhaps explain your reason for wanting unmanaged jars for the other targets?

tkw1536 commented 5 years ago

/cc @Jazzpirate

makarius commented 5 years ago

On 08/10/18 16:45, Tom Wiesing wrote:

Of course there are dependencies that do not exist on sbt. As far as I know, these are:

  • isabelle jars

The Isabelle environment provides various jars for its own use, including the standard Scala library jars and another copy of xz-1.8.

When working with IntelliJ IDEA, I make sure that the environment is active: "isabelle env idea". Thus the sbt project setup will known about the presence of Isabelle. This might look odd from the Java standpoint, but Isabelle is much more than just jars (e.g. extra resources like etc/options).

There might be potential problems from overlapping jars of MMT vs. Isabelle with different versions, but so far it just happened to work. Maybe Java 11 modules will eventually solve such problems, but I don't understand this new concept yet.

Makarius
tkw1536 commented 5 years ago

The problems I am describing here occured before the Isabelle project was merged into devel.

I expect the big conflicts to come if MMT decides to update to Scala 2.13 and Isabelle does not (or vice-versa). This is due to the binary incompatibility of Scala.

tkw1536 commented 5 years ago

XZ is now available in tests. The problem was that paths to unmanaged jars were specified as a relative path. The tests were running in a subdirectory, hence this failed and they were unavailable.

Nonetheless the issue of having unmanaged jars in the first place remains.