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

--lossy-unification in Agda 2.6.3 #6337

Closed
martinescardo opened this issue Nov 16, 2022 · 5 comments · Fixed by #6339
Closed

--lossy-unification in Agda 2.6.3 #6337

martinescardo opened this issue Nov 16, 2022 · 5 comments · Fixed by #6339
Assignees
@andreasabel
Labels
PR welcome Welcome to submit a PR fixing this issue release blocker Issues blocking the next Agda release ux: options Issues relating to Agda's command line options
Milestone
2.6.3

Comments

@martinescardo
Copy link

Agda developers, thanks for accommodating the renaming of --experimental-lossy-unification to --lossy-unification, which I asked for in a separate issue.

Which I now realize will cause a problem for a few of us, not only in my project TypeTopology, but (at least) the cubical library.

I wonder if we could still keep --experimental-lossy-unification as "deprecated" but still functional for a while, until everybody transitions from 2.6.2.2 to 2.6.3, which, of course, is going to take a while. We don't want to give trouble to our library users. Thank you.
@andreasabel andreasabel added this to the 2.6.3 milestone Nov 17, 2022
@andreasabel andreasabel added the release blocker Issues blocking the next Agda release label Nov 17, 2022
@andreasabel
Copy link
Member

Yeah, makes sense to not bluntly remove syntax from one release to another, and this also applies to command-line and pragma syntax. (With some hesitation whether this principle should also apply to experimental, undocumented features like --lossy-unification.)

Shouldn't be hard to add a mechanism for the substitution old-flag --> new-flag that comes with a deprecation warning.

@andreasabel andreasabel added PR welcome Welcome to submit a PR fixing this issue ux: options Issues relating to Agda's command line options labels Nov 17, 2022
@andreasabel andreasabel self-assigned this Nov 19, 2022
@andreasabel
Copy link
Member

Chefsache.

@andreasabel andreasabel mentioned this issue Nov 19, 2022
Merged
andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
Refactor for #6337: simplify checkOpts and unsafePragmaOptions
f7f84ac 
`checkOpts` is just excluding `--vim` and `--only-scope-checking`, it does
not modify the options record any longer (maybe did so in the past).
Thus, it's type can be simply `m ()` (for a `MonadError m`).

`unsafePragmaOptions` took `CommandLineOptions` as arguments but ignored
it, so I zapped it.  This allowed to simplify code elsewhere.
@andreasabel andreasabel mentioned this issue Nov 19, 2022
Merged
andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
Refactor for #6337: simplify checkOpts and unsafePragmaOptions
6ed10c5 
`checkOpts` is just excluding `--vim` and `--only-scope-checking`, it does
not modify the options record any longer (maybe did so in the past).
Thus, it's type can be simply `m ()` (for a `MonadError m`).

`unsafePragmaOptions` took `CommandLineOptions` as arguments but ignored
it, so I zapped it.  This allowed to simplify code elsewhere.
andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
Refactor for #6337: simplify checkOpts and unsafePragmaOptions
3552025 
`checkOpts` is just excluding `--vim` and `--only-scope-checking`, it does
not modify the options record any longer (maybe did so in the past).
Thus, it's type can be simply `m ()` (for a `MonadError m`).

`unsafePragmaOptions` took `CommandLineOptions` as arguments but ignored
it, so I zapped it.  This allowed to simplify code elsewhere.
andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
New for #6337: Agda.Utils.Monad.tell1
8cd7141
andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
Clean (re #6337): remove dead #if -- we use QuickCheck >= 2.14
60a391d
andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
Fix #6337: infrastructure for renamed options and option warnings
cd546d4 
It is more user-friendly to not flatly rename a commandline or pragma
option, but to keep the old name around with a deprecation warning.

This commit sets up the necessary infrasturcture and applies it to the
renaming from --experimental-lossy-unification to --lossy-unification.

Also adds the first testcase for the --lossy-unification feature.
@andreasabel
Copy link
Member

Price tag on this issue: 5000 SEK
(One of my hours costs GU 1000 SEK.)

andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
Refactor for #6337: simplify checkOpts and unsafePragmaOptions
e71c3e2 
`checkOpts` is just excluding `--vim` and `--only-scope-checking`, it does
not modify the options record any longer (maybe did so in the past).
Thus, it's type can be simply `m ()` (for a `MonadError m`).

`unsafePragmaOptions` took `CommandLineOptions` as arguments but ignored
it, so I zapped it.  This allowed to simplify code elsewhere.
andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
New for #6337: Agda.Utils.Monad.tell1
0a71545
andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
Clean (re #6337): remove dead #if -- we use QuickCheck >= 2.14
1f68693
andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
Fix #6337: infrastructure for renamed options and option warnings
48fcdd5 
It is more user-friendly to not flatly rename a commandline or pragma
option, but to keep the old name around with a deprecation warning.

This commit sets up the necessary infrasturcture and applies it to the
renaming from --experimental-lossy-unification to --lossy-unification.

Also adds the first testcase for the --lossy-unification feature.
andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
Refactor for #6337: simplify checkOpts and unsafePragmaOptions
78bff3a 
`checkOpts` is just excluding `--vim` and `--only-scope-checking`, it does
not modify the options record any longer (maybe did so in the past).
Thus, it's type can be simply `m ()` (for a `MonadError m`).

`unsafePragmaOptions` took `CommandLineOptions` as arguments but ignored
it, so I zapped it.  This allowed to simplify code elsewhere.
andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
New for #6337: Agda.Utils.Monad.tell1
39ffff3
andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
Clean (re #6337): remove dead #if -- we use QuickCheck >= 2.14
0ba8488
andreasabel added a commit that referenced this issue Nov 19, 2022
@andreasabel
Fix #6337: infrastructure for renamed options and option warnings
c6e45e9 
It is more user-friendly to not flatly rename a commandline or pragma
option, but to keep the old name around with a deprecation warning.

This commit sets up the necessary infrasturcture and applies it to the
renaming from --experimental-lossy-unification to --lossy-unification.

Also adds the first testcase for the --lossy-unification feature.
@martinescardo
Copy link
Author

Price tag on this issue: 5000 SEK (One of my hours costs GU 1000 SEK.)

Thanks a lot for doing this. I am applying for a grant to pay for this. But I can also pay you with my hours in the future.

@asr
Copy link
Member

asr commented Nov 21, 2022

@andreasabel, I suggest to create an issue with milestone 2.6.4 for removing the --experimental-lossy-unification option.

@asr asr changed the title --lossy-unification in Agda 2.6.3 --lossy-unification in Agda 2.6.3 Jan 23, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andreasabel andreasabel

Labels
PR welcome Welcome to submit a PR fixing this issue release blocker Issues blocking the next Agda release ux: options Issues relating to Agda's command line options
Projects
None yet
Milestone
2.6.3
Development

Successfully merging a pull request may close this issue.

Fix #6337: keep old option name, but deprecate it agda/agda
3 participants
@asr @andreasabel @martinescardo