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

Warn on unused variables in Ltac2 #18637

Open
rlepigre opened this issue Feb 8, 2024 · 1 comment · May be fixed by #18641
Open

Warn on unused variables in Ltac2 #18637

rlepigre opened this issue Feb 8, 2024 · 1 comment · May be fixed by #18641
Labels
kind: feature New user-facing feature request or implementation. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.

Comments

@rlepigre
Copy link
Contributor

rlepigre commented Feb 8, 2024

That is something @Janno and I keep wanting to have.
@rlepigre rlepigre added kind: feature New user-facing feature request or implementation. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. labels Feb 8, 2024
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Feb 8, 2024
@SkySkimmer
Ltac2: warn on unused variables
abb4247 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Feb 8, 2024
@SkySkimmer
Ltac2: warn on unused variables
5176cf3 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

TODO: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...` just `x` would be nicer.
@SkySkimmer SkySkimmer linked a pull request Feb 8, 2024 that will close this issue
Open
@SkySkimmer
Copy link
Contributor

Please comment on the design decision mentioned in #18641

SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Feb 19, 2024
@SkySkimmer
Ltac2: warn on unused variables
93d0b93 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

TODO: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...` just `x` would be nicer.
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Feb 20, 2024
@SkySkimmer
Ltac2: warn on unused variables
4ec4a56 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

TODO: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...` just `x` would be nicer.
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Feb 20, 2024
@SkySkimmer
Ltac2: warn on unused variables
cf6fd9d 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

TODO: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...` just `x` would be nicer.
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Feb 22, 2024
@SkySkimmer
Ltac2: warn on unused variables
bb1a636 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Feb 22, 2024
@SkySkimmer
Ltac2: warn on unused variables
4bc7909 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
rlepigre pushed a commit to rlepigre/coq that referenced this issue Mar 7, 2024
@SkySkimmer @rlepigre
Ltac2: warn on unused variables
04298a3 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
rlepigre pushed a commit to rlepigre/coq that referenced this issue Mar 7, 2024
@SkySkimmer @rlepigre
Ltac2: warn on unused variables
03705f9 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
rlepigre pushed a commit to rlepigre/coq that referenced this issue Mar 7, 2024
@SkySkimmer @rlepigre
Ltac2: warn on unused variables
11a49b9 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
rlepigre pushed a commit to rlepigre/coq that referenced this issue Mar 7, 2024
@SkySkimmer @rlepigre
Ltac2: warn on unused variables
cfa6af3 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
rlepigre pushed a commit to rlepigre/coq that referenced this issue Mar 12, 2024
@SkySkimmer @rlepigre
Ltac2: warn on unused variables
412e4aa 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
rlepigre pushed a commit to rlepigre/coq that referenced this issue Mar 13, 2024
@SkySkimmer @rlepigre
Ltac2: warn on unused variables
35d212e 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
rlepigre pushed a commit to rlepigre/coq that referenced this issue Mar 13, 2024
@SkySkimmer @rlepigre
Ltac2: warn on unused variables
9dbb7a9 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
rlepigre pushed a commit to rlepigre/coq that referenced this issue Mar 14, 2024
@SkySkimmer @rlepigre
Ltac2: warn on unused variables
5abfd8f 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
rlepigre pushed a commit to rlepigre/coq that referenced this issue Mar 15, 2024
@SkySkimmer @rlepigre
Ltac2: warn on unused variables
382a6ad 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
rlepigre pushed a commit to rlepigre/coq that referenced this issue Mar 15, 2024
@SkySkimmer @rlepigre
Ltac2: warn on unused variables
25a0e6b 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
rlepigre pushed a commit to rlepigre/coq that referenced this issue Mar 15, 2024
@SkySkimmer @rlepigre
Ltac2: warn on unused variables
5df027c 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Mar 21, 2024
@SkySkimmer
Ltac2: warn on unused variables
be1b2c1 
Close coq#18637

To be decided:

- should we warn for variable names starting with `_`?
  (current code does)

- should we split the warning like ocaml does (unused `let x := ...`
  treated differently from unused `x` next to used `y` in
  `match ... with (x,y) => ...` or unused `x` in `fun x => ...`)

Future work: more precise locations, currently it's on the whole expression
ie all of `let x := ... in ...`, just `x` would be nicer.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: feature New user-facing feature request or implementation. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Ltac2: warn on unused variables SkySkimmer/coq
2 participants
@rlepigre @SkySkimmer