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

[fix] issue #1864 #1876

Merged
merged 1 commit into from
Nov 7, 2022
Merged

[fix] issue #1864 #1876

merged 1 commit into from
Nov 7, 2022

Conversation

jamesmckinna
Copy link
Contributor

No description provided.

@MatthewDaggitt
Copy link
Contributor

MatthewDaggitt commented Nov 7, 2022

So out of interest what was the actual problem here?

@MatthewDaggitt MatthewDaggitt merged commit ad757f9 into agda:master Nov 7, 2022
@jamesmckinna
Copy link
Contributor Author

See the issue #1864. The 'problem' you had identified was the imports being too heavy, so i thinned them out. But while I was doing that, I also saw that the structure of what is actually there is a lot of highly repetitive code for conjuring a decidable relation on a product out of decidable relations on its components. And that seems worth thinking about trying to refactor. So the PR as it stands/stood closed the original issue (as I understood it), while leaving the issue open with more work potentially to do... does that make sense?

@MatthewDaggitt
Copy link
Contributor

Yes, sorry, that was too terse of me! I meant what was actually the concrete import that caused the dependency cycles! But if you didn't identify it and just removed all that you could, that is also fine!

So the PR as it stands/stood closed the original issue (as I understood it), while leaving the issue open with more work potentially to do... does that make sense?

👍

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Nov 7, 2022

yes, i didn't do the analysis... except by the tried-and-true-but-brainless method of commenting out imports, and only reinstating locally the actual functions needing to be imported. But quite a lot, it seemed, could simply be deleted...

BTW, I never saw dependency cycles as such, so i wonder if that was a problem at your end?

@MatthewDaggitt
Copy link
Contributor

BTW, I never saw dependency cycles as such, so i wonder if that was a problem at your end?

No, I never saw dependency cycles, apologies if I wrote that. Its just that I was type-checking them and it was ending up type-checking half the standard library in order to do so. Which wasn't exactly great for code needed for writing tactics.

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

Successfully merging this pull request may close these issues.

2 participants