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

Problem with Imports #645

Closed
Timon555 opened this issue Apr 5, 2023 · 5 comments
Closed

Problem with Imports #645

Timon555 opened this issue Apr 5, 2023 · 5 comments

Comments

@Timon555
Copy link

Timon555 commented Apr 5, 2023

Importing a package from a folder to another folder in the same hierarchy is currently not possible.

@ArquintL
Copy link
Member

ArquintL commented Apr 5, 2023

Thanks for reporting this issue. I'm not sure what you exactly mean by "in the same hierarchy". Could you sketch a problematic folder structure or even provide a minimal example?
Thanks!

@Timon555
Copy link
Author

Timon555 commented Apr 5, 2023

Let's say we have a folder named Gobra that contains two subfolders. It's not possible to import something from a file in one subfolder to a file in the other subfolder.

@ArquintL
Copy link
Member

ArquintL commented Apr 5, 2023

Thanks for the clarification. Does this correspond to the setup in the "distributed_interface_case" test case (i.e. src/test/resources/regressions/features/interfaces/distributed_interface_case)?
There, the cellImplProof package imports, e.g., package cell.
While we use in-file configuration options to make the unit test work, you can achieve the same by passing -I <path to folder> to Gobra. In your case described above, you would use the path to the folder named Gobra.

@jcp19
Copy link
Contributor

jcp19 commented Apr 5, 2023

@Timon555 can you please provide enough information for us to be able to debug it in the future? In particular, please either provide the code here or a link to it and describe the error messages that you get

@jcp19
Copy link
Contributor

jcp19 commented Sep 21, 2023

Stale report without any relevant information.

@jcp19 jcp19 closed this as completed Sep 21, 2023
@jcp19 jcp19 closed this as not planned Won't fix, can't repro, duplicate, stale Sep 21, 2023
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

3 participants