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.

Sign up for GitHub

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

Jump to bottom

Auto missing support for Copatterns #957

Closed
GoogleCodeExporter opened this issue Aug 8, 2015 · 5 comments · Fixed by #5827
Closed

Auto missing support for Copatterns #957

GoogleCodeExporter opened this issue Aug 8, 2015 · 5 comments · Fixed by #5827
Assignees
@isovector
Labels
auto Issues to do with the Auto proof search (Mimer, Agsy) copatterns Definitions by copattern matching: projections on the LHS documented-in-changelog Issues already documented in the CHANGELOG type: enhancement Issues and pull requests about possible improvements
Milestone
2.6.3

Comments

@GoogleCodeExporter
Copy link 

git clone git@github.com:andreasabel/cubical.git -b 0.0.0.1

Load cubical/src/Control/Auto-Bug-in-Goal-2.agda

Fix the module name (should be Control.Auto-Bug-in-Goal-2).
Go to the second goal (?1).
Press C-c C-a.

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/Auto/Convert.hs:585

Original issue reported on code.google.com by andreas....@gmail.com on 13 Nov 2013 at 10:03
@GoogleCodeExporter
Copy link
Author 

This gives a proper error now.  TODO: make Agsy work with copatterns.

Original comment by andreas....@gmail.com on 22 Nov 2013 at 9:46

  • Changed title: Auto missing support for Copatterns
  • Added labels: Type-Enhancement
  • Removed labels: Type-Defect

@GoogleCodeExporter
Copy link
Author 

I talked to Fredrik today and he thinks it is not worth spending time on the 
current Auto since he has a new one.  He will do this after his thesis 
submission (sometime in Feb maybe)?

So, no milestone for 2.3.4.

Original comment by andreas....@gmail.com on 29 Nov 2013 at 3:38

  • Removed labels: Milestone-2.3.4

@GoogleCodeExporter GoogleCodeExporter added auto-migrated type: enhancement Issues and pull requests about possible improvements auto Issues to do with the Auto proof search (Mimer, Agsy) copatterns Definitions by copattern matching: projections on the LHS labels Aug 8, 2015
@GoogleCodeExporter
Copy link
Author

Original comment by andreas....@gmail.com on 29 Nov 2013 at 3:39

@UlfNorell UlfNorell mentioned this issue Sep 12, 2017
Closed
@UlfNorell UlfNorell added this to the icebox milestone May 24, 2018
@isovector
Copy link
Contributor

Without knowing anything about the internals, this feels like a rather arbitrary limitation. What would be necessary to get copatterns supported here?

@andreasabel
Copy link
Member

andreasabel commented Mar 11, 2022 •
edited
Loading

What would be necessary to get copatterns supported here?

Understand and extend the Agda.Auto.* implementation. No one has been willing to do that; Auto is bit-rotting. If you look at the code, you might understand why.
@UlfNorell has a student working on a new term synthesizer.

@isovector isovector mentioned this issue Mar 11, 2022
Merged
andreasabel pushed a commit that referenced this issue Mar 16, 2022
@isovector
Fix #957: Agsy copattern support (#5827)
2816605
@jespercockx jespercockx modified the milestones: icebox, 2.6.3 Aug 24, 2022
@andreasabel andreasabel mentioned this issue Oct 24, 2022
Closed
@andreasabel andreasabel added the documented-in-changelog Issues already documented in the CHANGELOG label Oct 25, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@isovector isovector

Labels
auto Issues to do with the Auto proof search (Mimer, Agsy) copatterns Definitions by copattern matching: projections on the LHS documented-in-changelog Issues already documented in the CHANGELOG type: enhancement Issues and pull requests about possible improvements
Projects
None yet
Milestone
2.6.3
Development

Successfully merging a pull request may close this issue.

Fix #957: Agsy copattern support
5 participants
@isovector @UlfNorell @andreasabel @jespercockx @GoogleCodeExporter