8000 Make unqualified JSON goal types by isovector · Pull Request #5776 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Make unqualified JSON goal types #5776

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
Merged
merged 2 commits into from
Feb 24, 2022
Merged

Make unqualified JSON goal types #5776

merged 2 commits into from
Feb 24, 2022

Conversation

isovector
Copy link
Contributor
@isovector isovector commented Feb 4, 2022 •
edited
Loading

Fixes #5775

I don't pretend to know what's happening here, I'm just cargo culting from the emacs codepath.

The previously pathological output (detailed in the issue) is now

Visible Goals:
?0 : map In (map (fold (map In)) (inᵒ x)) ≡ fold (map In) (In (inᵒ x))
?1 : inᵒ x ≡ map In (map (fold (map In)) (inᵒ x))

@isovector isovector marked this pull request as draft February 4, 2022 02:01
@isovector isovector marked this pull request as ready for review February 4, 2022 06:30
@andreasabel andreasabel requested a review from ice1000 February 6, 2022 10:22
@andreasabel
Copy link
Member

@Mergifyio rebase

@mergify
Copy link
mergify bot commented Feb 10, 2022

rebase

✅ Branch has been successfully rebased

@andreasabel andreasabel requested a review from rwe February 11, 2022 10:21
@andreasabel
Copy link
Member

@rwe @msuperdock : Anyone willing to review?
(I do not know about the goals and principles of interaction-json, so I cannot say anything qualified, I could just merge this optimistically.)

@andreasabel
Copy link
Member

@isovector : There seems no reviewer around, so I will just merge once you say it is ready.

@isovector
Copy link
Contributor Author

@andreasabel I think it's ready. I've been using it daily since submitting this PR and have seen no issues with it. Thanks!

@isovector isovector mentioned this pull request Feb 16, 2022
Closed
@msuperdock
Copy link
Contributor

For what it's worth, I'm generally on board with making changes to JSONTop.hs that make the parts of the JSON output more closely match the emacs output, and I think others involved with --interaction-json would agree.

@isovector, could you point out the corresponding lines in the emacs interaction code?

@isovector
Copy link
Contributor Author

@msuperdock emacs calls showGoals:

agda/src/full/Agda/Interaction/EmacsTop.hs

Line 127 in d4333bb

goals <- showGoals ms

which in turn does the same thing I'm doing here:

agda/src/full/Agda/Interaction/BasicOps.hs

Lines 737 to 739 in d4333bb

di <- forM ims $ \ i ->
withInteractionId (outputFormId $ OutputForm noRange [] alwaysUnblock i) $
prettyATop i

@msuperdock
Copy link
Contributor
msuperdock commented Feb 18, 2022 •
edited
Loading

Thanks for showing this. I see that the other commit also imitates the emacs mode:

agda/src/full/Agda/Interaction/EmacsTop.hs

Line 196 in d4333bb

Info_GoalSpecific ii kind -> lispifyGoalSpecificDisplayInfo ii kind

I haven't tested this pull request, but I would be happy for it to be merged!

@isovector
Copy link
Contributor Author

@andreasabel this is ready to be merged!

@andreasabel andreasabel merged commit 56de2d5 into agda:master Feb 24, 2022
@andreasabel andreasabel added this to the 2.6.3 milestone Feb 24, 2022
andreasabel pushed a commit that referenced this pull request Mar 15, 2022
@isovector @andreasabel
Make unqualified JSON goal types (#5776)
da72a2d
andreasabel pushed a commit that referenced this pull request Mar 16, 2022
@isovector @andreasabel
Make unqualified JSON goal types (#5776)
f4b1234
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ice1000 ice1000 Awaiting requested review from ice1000

@rwe rwe Awaiting requested review from rwe

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
2.6.3
Development

Successfully merging this pull request may close these issues.

JSON interaction produces fully qualified terms
3 participants
@isovector @andreasabel @msuperdock
0