Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Including verification dependencies breaks imports #807

Open
HSMF opened this issue Dec 7, 2024 · 0 comments
Open

Including verification dependencies breaks imports #807

HSMF opened this issue Dec 7, 2024 · 0 comments

Comments

@HSMF
Copy link

HSMF commented Dec 7, 2024

In a setup containing nested projects, such as when including dependencies as git submodules, importing packages from that dependency is not possible.

Below is a simplified structure from including viperproject/gobra-libs:

├── main.gobra
└── pkg
    ├── math
    │   └── math.gobra
    └── util
        └── util.gobra

main.gobra

package main
//+gobra

import "pkg/math"

func client() {
	assert math.Bar() == 1
}

pkg/util/util.gobra

package util
//+gobra

ghost
decreases
pure func Foo() int {
	return 1
}

pkg/math/math.gobra

package math
//+gobra

import "util"

ghost
decreases
pure func Bar() int {
	return util.Foo()
}

Verifying pkg on its own works fine: Running gobra -r -I . in pkg yields no errors.

Verifying the client project, however, does not work: gobra -I . -p . yields the following error:

19:13:19.993 [thread-6] ERROR viper.gobra.reporting.FileWriterReporter - Error at: <./pkg/math/math.gobra:4:8> ./pkg/math/math.gobra:4:8:error: Explicit qualifier could not be derived (reason: 'No existing directory found for import path 'util'')
import "util"
       ^

19:13:20.000 [thread-14] ERROR viper.gobra.reporting.FileWriterReporter - Error at: <./main.gobra:3:8> ./main.gobra:3:8:error: Package contains 1 error(s): ./pkg/math/math.gobra:4:8:error: Explicit qualifier could not be derived (reason: 'No existing directory found for import path 'util'')
import "util"
       ^

import "pkg/math"
       ^

Note that changing the import in pkg/math from import "util" to import "pkg/util" is not sufficient, as this will break verification of pkg on its own.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant