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

[sercomp] Unify sercomp and compser by adding input option to sercomp #120

Merged
merged 1 commit into from
Mar 13, 2019
Merged

[sercomp] Unify sercomp and compser by adding input option to sercomp #120

merged 1 commit into from
Mar 13, 2019

Conversation

palmskog
Copy link
Collaborator

@palmskog palmskog commented Mar 13, 2019 •
edited
Loading

This paves the way for more easily adding more input and output formats to sercomp as discussed in #119. Also adds some more documentation.

Fixes #111.

@palmskog palmskog requested a review from ejgallego March 13, 2019 00:05
@palmskog palmskog changed the title Unify sercomp and compser by adding input option to sercomp [sercomp] Unify sercomp and compser by adding input option to sercomp Mar 13, 2019
@palmskog palmskog added this to the 0.6.1 milestone Mar 13, 2019
@ejgallego ejgallego self-assigned this Mar 13, 2019
ejgallego
ejgallego reviewed Mar 13, 2019
View reviewed changes
sertop/sertop_arg.ml
let comp_input_args =
Arg.(enum
[ "vernac", I_vernac
; "sexp", I_sexp])
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit on indentation.

ejgallego
ejgallego approved these changes Mar 13, 2019
View reviewed changes
Copy link
Owner

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Great thanks! I think we may refine a bit more, maybe adding an --output flag?

This way, input, processing, and output would be decoupled. But indeed this is good as-is; we may see what we do once we use the new document manager.

@ejgallego ejgallego merged commit 90f28cc into v8.9 Mar 13, 2019
@ejgallego ejgallego deleted the v8.9+unified_sercomp branch March 13, 2019 15:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ejgallego ejgallego ejgallego approved these changes

Assignees

@ejgallego ejgallego

Labels
kind: documentation kind: enhancement
Projects
None yet
Milestone
0.6.1
Development

Successfully merging this pull request may close these issues.
2 participants
@palmskog @ejgallego