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

Documentation says --sized-types is the default when it isn't #6250

Closed
andreasabel opened this issue Oct 28, 2022 · 1 comment · Fixed by #6255
Closed

Documentation says --sized-types is the default when it isn't #6250

andreasabel opened this issue Oct 28, 2022 · 1 comment · Fixed by #6255
Assignees
@andreasabel
Labels
guardedness Problems of the guardedness checker for coinduction. regression in 2.6.2 Regression that first appeared in Agda 2.6.2 sized types Sized types, termination checking with sized types, size inference ux: documentation Issues relating to Agda's documentation
Milestone
2.6.3

Comments

@andreasabel
Copy link
Member

In 7bc9192 (@jespercockx) --no-sized-types was made the default, but the documentation still says the opposite.

agda/doc/user-manual/tools/command-line-options.rst

Lines 532 to 541 in abaeefd

.. option:: --sized-types, --no-sized-types
Enable [disable] sized types (see :ref:`sized-types`).
The option ``--sized-types`` is inconsistent with
constructor-based guarded corecursion and it is turned off by
:option:`--safe` (but can be turned on again, as long as not also
:option:`--guardedness` is on).
Default: ``--sized-types``

Same for --guardedness:

agda/doc/user-manual/tools/command-line-options.rst

Lines 453 to 462 in abaeefd

.. option:: --guardedness, --no-guardedness
Enable [disable] constructor-based guarded corecursion (see
:ref:`coinduction`).
The option ``--guardedness`` is inconsistent with sized types and
it is turned off by :option:`--safe` (but can be turned on again,
as long as not also :option:`--sized-types` is on).
Default: ``--guardedness``

The --help text is likewise outdated.
@andreasabel andreasabel added sized types Sized types, termination checking with sized types, size inference ux: documentation Issues relating to Agda's documentation not-in-changelog This issue should not be listed in the changelog. guardedness Problems of the guardedness checker for coinduction. regression in 2.6.2 Regression that first appeared in Agda 2.6.2 labels Oct 28, 2022
@andreasabel andreasabel added this to the 2.6.3 milestone Oct 28, 2022
@andreasabel andreasabel self-assigned this Oct 28, 2022
@andreasabel andreasabel removed the not-in-changelog This issue should not be listed in the changelog. label Oct 28, 2022
@andreasabel
Copy link
Member Author

(Actually, why shouldn't this go into the changelog.)

andreasabel added a commit that referenced this issue Oct 28, 2022
@andreasabel
Fix #6250 fix #6251: neither --sized-types nor --guardedness is default
105d8d7 
Also remove mentions of --subtyping.
@andreasabel andreasabel mentioned this issue Oct 28, 2022
Merged
andreasabel added a commit that referenced this issue Oct 29, 2022
@andreasabel
Fix #6250 fix #6251: neither --sized-types nor --guardedness is default
172366d 
Also remove mentions of --subtyping.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
guardedness Problems of the guardedness checker for coinduction. regression in 2.6.2 Regression that first appeared in Agda 2.6.2 sized types Sized types, termination checking with sized types, size inference ux: documentation Issues relating to Agda's documentation
Projects
None yet
Milestone
2.6.3
Development

Successfully merging a pull request may close this issue.

Help/doc: neither --sized-types nor --guardedness is default agda/agda
1 participant
@andreasabel