epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
349 stars 49 forks source link

Move Inox as a submodule instead of an http dependency #1520

Closed samuelchassot closed 2 months ago

vkuncak commented 2 months ago

For the future or in case things go wrong: @samuelchassot , can you summarize the advantages of this over the current approach with hash commit?

vkuncak commented 2 months ago

@sankalpgambhir @drganam just making sure you are up to date with this change as well, since you are working on adding functionality at the Inox level. Let @samuelchassot know if you agree with this new way of managing inox as a dependency.

sankalpgambhir commented 2 months ago

I think it's a good change! It would simplify testing Stainless and Inox together. With the current dependency setup, you often end up with sbt recompiling Inox entirely on any changes. I expect that having it as a subproject works better wrt these issues.

drganam commented 2 months ago

Sounds great, I agree with this change!

samuelchassot commented 2 months ago

The main point is to add Inox as a submodule of the Stainless repository so that Inox's source is part of the Stainless repository.

Pros: Given how tightly coupled Inox is with Stainless, Inox is not modularised from the Stainless perspective. Therefore, it makes sense for Inox to be part of the Stainless source.

Cons:

vkuncak commented 2 months ago

@samuelchassot please just rebase and we can merge

samuelchassot commented 2 months ago

The conflict came from the new warning added to say we don't support Scala 2 anymore, which happened to be in the same spot as the warning about the git submodule.