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

Frontend documentation #766

Merged
merged 3 commits into from
Jul 27, 2023
Merged

Conversation

Halbaroth
Copy link
Collaborator

No description provided.

@Halbaroth Halbaroth added this to the 2.5.0 milestone Jul 27, 2023
@Halbaroth
Copy link
Collaborator Author

Halbaroth commented Jul 27, 2023

I removed the adjective fully to qualify the new support of the SMT-LIB language with Dolmen. Indeed, we fully support the parsing and typing but there are plenty of SMT-LIB statements ignored by AE.

Copy link
Collaborator

@bclement-ocp bclement-ocp left a comment

Choose a reason for hiding this comment

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

LGTM with some minor stylistic changes


### Frontend option

The `--frontend` option let's you select the frontend used to parse and type the input file. Since 2.5.0,
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
The `--frontend` option let's you select the frontend used to parse and type the input file. Since 2.5.0,
The `--frontend` option let's you select the frontend used to parse and type the input file. Since version 2.5.0,

The `--frontend` option let's you select the frontend used to parse and type the input file. Since 2.5.0,
Alt-Ergo integrates two frontends:
- The `legacy` frontend is the historical frontend of Alt-Ergo supporting the native language
and (partially) supporting the SMT-LIB language. The legacy frontend is selected by default.
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
and (partially) supporting the SMT-LIB language. The legacy frontend is selected by default.
and (partially) supporting the SMT-LIB language. The legacy frontend is currently the default.

Comment on lines 34 to 35
You can select it with the `--frontend dolmen` option. In the future, this
frontend will be used by default.
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
You can select it with the `--frontend dolmen` option. In the future, this
frontend will be used by default.
You can select it with the `--frontend dolmen` option, which is planned to become the default in a future release.

@Halbaroth Halbaroth enabled auto-merge (squash) July 27, 2023 14:53
@Halbaroth Halbaroth merged commit e7ce642 into OCamlPro:next Jul 27, 2023
8 checks passed
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this pull request Jul 28, 2023
* Update the frontend documentation

* Removing the `fully` adjective

* Review changes
@Halbaroth Halbaroth mentioned this pull request Jul 28, 2023
@Halbaroth Halbaroth mentioned this pull request Aug 23, 2023
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