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

use prettyShow instead of show for JSON solveAll #5752

Merged
merged 1 commit into from
Jan 25, 2022
Merged

use prettyShow instead of show for JSON solveAll #5752

merged 1 commit into from
Jan 25, 2022

Conversation

isovector
Copy link
Contributor

@isovector isovector commented Jan 25, 2022 •
edited
Loading

Probably fixes #5751. But I'm new to this codebase and am not sure how to go about testing it except manually --- would love some tips!

Indeed, this seems to fix the output:

JSON> IOTCM "/home/sandy/prj/agda-playground/ConceptualMathematics/Chapter1.agda" None Direct (Cmd_solveOne Simplified 0 noRange "")
{"kind":"SolveAll","solutions":[{"expression":"g kIso (f kIso (gIso .g x))","interactionPoint":0}]}

@andreasabel andreasabel added the interaction-json JSON protocol for communicating with Agda label Jan 25, 2022
@andreasabel andreasabel merged commit 72e26d4 into agda:master Jan 25, 2022
@ice1000
Copy link
Member

ice1000 commented Jan 25, 2022

Thank you!

@isovector isovector mentioned this pull request Feb 16, 2022
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ice1000 ice1000 ice1000 left review comments

@andreasabel andreasabel andreasabel left review comments

Assignees
No one assigned
Labels
interaction-json JSON protocol for communicating with Agda
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

json interaction produces Haskell output for SolveAll
3 participants
@isovector @ice1000 @andreasabel