aya-prover / aya-dev

A proof assistant and a dependently-typed language
https://www.aya-prover.org
MIT License
281 stars 16 forks source link

Recursive import causes StackOverflow #750

Open ice1000 opened 1 year ago

ice1000 commented 1 year ago

Just try.

mio-19 commented 1 year ago

Should them be disallowed?

ice1000 commented 1 year ago

Yes, I believe so :)

ice1000 commented 1 year ago

This can be solved by adding a new phase in library import resolving.

mio-19 commented 1 year ago

How about detecting them on the fly?

imkiva commented 1 year ago

Do you mean import modules recursively in a library or import a file in SingleAyaFile?

imkiva commented 1 year ago

Any stacktrace would be helpful

ice1000 commented 1 year ago

Do you mean import modules recursively in a library or import a file in SingleAyaFile?

The former

ice1000 commented 1 year ago

Any stacktrace would be helpful

I'll provide some later

ice1000 commented 1 year ago
diff --git a/base/src/test/resources/success/nonsense/src/Nonsense/A.aya b/base/src/test/resources/success/nonsense/src/Nonsense/A.aya
new file mode 100644
index 000000000..44692bed3
--- /dev/null
+++ b/base/src/test/resources/success/nonsense/src/Nonsense/A.aya
@@ -0,0 +1 @@
+import Nonsense::B
\ No newline at end of file
diff --git a/base/src/test/resources/success/nonsense/src/Nonsense/B.aya b/base/src/test/resources/success/nonsense/src/Nonsense/B.aya
new file mode 100644
index 000000000..e8c2e0d9b
--- /dev/null
+++ b/base/src/test/resources/success/nonsense/src/Nonsense/B.aya
@@ -0,0 +1 @@
+import Nonsense::A
ice1000 commented 1 year ago

Then, load nonsense/src/Nonsense/A.aya or nonsense/src/Nonsense/B.aya