assumption?

[jalex-stark]

See this topic and this topic on zulip.

[jalex-stark]

this file is actually garbage, I don't know how to get the output of the test

[gebner]

cd tests/lean
./test_single.sh ../../bin/lean assumption.lean

[gebner]

The output is still wrong. Please fix it until the command above prints -- checked.

[jalex-stark]

hmm actually I still don't know how to build bin/lean in the first place
probably it's these instructions
https://github.com/leanprover-community/lean/blob/master/doc/make/index.md#generic-build-instructions

[gebner]

Yes, where are you stuck?

[jalex-stark]

now I'm just waiting on the build. before I was stuck on understanding the error messages that came out of ./test_single.sh ../../bin/lean assumption.lean

[jalex-stark]

Now I have a real lean binary. I'm getting "error: unexpected token" at the question mark. Most of my debugging strategies rely on VSCode; is there a way to tell it to use the local lean binary?

[jalex-stark]

Hmm. Seems like the current commit gives lots of errors like this. I thought the approach using the optional parse argument would prevent these. I think I should give up.

/Users/jstark/lean-projects/lean/library/init/meta/interactive.lean:1057:30: error: type mismatch at application
  try assumption
term
  assumption
has type
  parse (tk "?")? → tactic unit
but is expected to have type
  itactic

[gebner]

I think you should just replace these references to assumption by tactic.assumption. The ? parser only works when the tactic is parsed in an begin ... end block (or by ...).

[jalex-stark]

Okay, I think I have implemented that suggestion in the latest commit. I'm still getting the following, which seems to be the opposite problem (i want it to use the version with the parser and it uses the version without) I tried adding import tactic.interactive but i could not resolve that import.

/Users/jstark/lean-projects/lean/tests/lean/assumption.lean:3:12: error: unexpected token
/Users/jstark/lean-projects/lean/tests/lean/assumption.lean:4:0: error: invalid 'end', there is no open namespace/section

[gebner]

I feel obligated to mention that you could also implement assumption? in mathlib using the trick described here.

[gebner]

bors try

[bors]

try

Build failed:

• Build linux Release

[gebner]

bors try

[bors]

try

Build failed:

• Build linux Release

[gebner]

I think for the ? notation to work, you need to add this before assumption: (copied from rcases)

precedence `?`:max

You should also add an assumption' tactic (of type tactic unit) that you can use as auto_param. That is, replace . assumption by . assumption' in two tests.

[jalex-stark]

I think for the ? notation to work, you need to add this before assumption: (copied from rcases)

precedence `?`:max

You should also add an assumption' tactic (of type tactic unit) that you can use as auto_param. That is, replace . assumption by . assumption' in two tests.

There's currently an assumption' tactic that's essentially all_goals {assumption}. which one deserves the name?
(I don't know what an auto_param is, and I don't know which two tests you want replaced.)

[gebner]

If you write . assumption after the type of an argument, then Lean will try to automatically fill in the argument by calling the tactic assumption. This is also works for structure fields.

There are two tests that use . assumption (just search for it). The auto_param is definitely the least important, the current assumption' should stay as it is.

[jalex-stark]

If you write . assumption after the type of an argument, then Lean will try to automatically fill in the argument by calling the tactic assumption. This is also works for structure fields.

There are two tests that use . assumption (just search for it). The auto_param is definitely the least important, the current assumption' should stay as it is.

so these tests need . assumption replaced by . tactic.assumption? or we should make assumption'' an alias for tactic.assumption? (I don't really know what's going on and my instinct is to blindly try to implement what you tell me.)

[jalex-stark]

in the latest commit, I have
./test_single.sh ../../bin/lean assumption.lean gives output -- checked

but the . assumption tests are I think still broken, working on it.

[gebner]

I think you should add an assumption'' and use that in the tests.

bors try

[bors]

try

Build failed:

• Build linux Release

[gebner]

Oh wow, the precedence change broke a lot of stuff. You should post a message on Zulip about this. I'm not sure what the correct solution here is.

[jalex-stark]

I feel obligated to mention that you could also implement assumption? in mathlib using the trick described here.

Maybe this approach would get around the current problem. Note that rcases is in mathlib and the precedence stuff doesn't break there.