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

Pantograph Error Cases Report #53

Open
1 of 2 tasks
RexWzh opened this issue Dec 19, 2024 · 14 comments
Open
1 of 2 tasks

Pantograph Error Cases Report #53

RexWzh opened this issue Dec 19, 2024 · 14 comments
Labels
bug Something isn't working help wanted Extra attention is needed

Comments

@RexWzh
Copy link

RexWzh commented Dec 19, 2024 •
edited
Loading

Environment setup

header = """
set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat
"""
project_path = "<repo>/experiments/minif2f/MiniF2F"
server = Server(imports=['Aesop', 'Mathlib'], project_path=project_path)

Error cases

  • JSONDecodeError for some cases

    theorem amc12_2000_p15 (f : ℂ → ℂ) (h₀ : ∀ x, f (x / 3) = x ^ 2 + x + 1)
    (h₁ : Fintype (f ⁻¹' {7})) : (∑ y in (f ⁻¹' {7}).toFinset, y / 3) = -1 / 9

theorem mathd_numbertheory_552
  (f g h : ℕ+ → ℕ)
  (h₀ : ∀ x, f x = 12 * x + 7)
  (h₁ : ∀ x, g x = 5 * x + 2)
  (h₂ : ∀ x, h x = Nat.gcd (f x) (g x))
  (h₃ : Fintype (Set.range h)) :
  (∑ k in (Set.range h).toFinset, k) = 12

    A minimized Case

    theorem mathd_numbertheory_552_min (h : ℕ → ℕ) (h₃ : Fintype (Set.range h)) : true

  • Unsolved goals

    theorem sample (p q r x : ℂ)
      (h₀ : (x - p) * (x - q) = (r - p) * (r - q))
   : (x - r) * x = (x - r) * (p + q - r) := by
linear_combination h₀

    The remaining goal state:

    p : ℂ
q : ℂ
r : ℂ
x : ℂ
h₀ : (x - p) _(x - q) = (r - p)_ (r - q)
⊢ ℂ

Lean Server Result

The Lean server response can be check here
image
@Purewhite2019
Copy link

As for the JSONDecodeError in mathd_numbertheory_552 (and the corrsponding MWE), could you please try the following fix?

https://github.com/lenianiva/PyPantograph/blob/f4cc21cc963a9f410b0aec05052d6b4975861321/pantograph/server.py#L177

@lenianiva
Copy link
Member

Can you explain what is supposed to happen in case 2?

The first one is probably a Python problem

@RexWzh
Copy link
Author

RexWzh commented Dec 20, 2024 •
edited
Loading

The first one is probably a Python problem

@Purewhite2019
The error is raised by the server, not by json-loading. You can reproduce the error by:

thm = """theorem amc12_2000_p15 (f : ℂ → ℂ) (h₀ : ∀ x, f (x / 3) = x ^ 2 + x + 1)
    (h₁ : Fintype (f ⁻¹' {7})) : (∑ y in (f ⁻¹' {7}).toFinset, y / 3) = -1 / 9 := sorry
"""
unit = server.load_sorry(thm)[0]
Traceback (most recent call last):
  File "/home/cubelab/workspace/Lean/PyPantograph/pantograph/server.py", line 133, in run
    obj = json.loads(line)
  File "/home/cubelab/miniconda3/envs/p2g/lib/python3.10/json/__init__.py", line 346, in loads
    return _default_decoder.decode(s)
  File "/home/cubelab/miniconda3/envs/p2g/lib/python3.10/json/decoder.py", line 337, in decode
    obj, end = self.raw_decode(s, idx=_w(s, 0).end())
  File "/home/cubelab/miniconda3/envs/p2g/lib/python3.10/json/decoder.py", line 355, in raw_decode
    raise JSONDecodeError("Expecting value", s, err.value) from None
json.decoder.JSONDecodeError: Expecting value: line 1 column 1 (char 0)

More precisely, it might be caused by the () in the last condition:

(∑ y in (f ⁻¹' {7}).toFinset, y / 3)

The same applies to the second one. Note that these cases work fine in the Lean Server.

import Mathlib
import Aesop

theorem mathd_numbertheory_552
  (f g h : ℕ+ → ℕ)
  (h₀ : ∀ x, f x = 12 * x + 7)
  (h₁ : ∀ x, g x = 5 * x + 2)
  (h₂ : ∀ x, h x = Nat.gcd (f x) (g x))
  (h₃ : Fintype (Set.range h)) :
  (∑ k in (Set.range h).toFinset, k) = 12 := sorry

theorem amc12_2000_p15 (f : ℂ → ℂ) (h₀ : ∀ x, f (x / 3) = x ^ 2 + x + 1)
    (h₁ : Fintype (f ⁻¹' {7})) : (∑ y in (f ⁻¹' {7}).toFinset, y / 3) = -1 / 9 := sorry

@Purewhite2019
Copy link

The error is raised by the server, not by json-loading. You can reproduce the error by:

Understood. This does seem rather strange as I've come across several similar issues that were due to json errors and were resolved by setting ensure_ascii=False.

I was able to successfully reproduce the error you mentioned. Below is a more detailed error backtrace:

PANIC at _private.Pantograph.Frontend.MetaTranslate.0.Pantograph.Frontend.MetaTranslate.translateExpr Pantograph.Frontend.MetaTranslate:71:6: assertion violation: ( [email protected]._hyg.610.0 ).contains fvarId'

      
backtrace:
/path/to/pantograph/pantograph-repl(lean_panic_fn+0x70) [0xaaaad8c6b250]
/path/to/pantograph/pantograph-repl(l_panic___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__1+0x44) [0xaaaad53c26c4]
/path/to/pantograph/pantograph-repl(lean_apply_7+0x460) [0xaaaad8c7a890]
/path/to/pantograph/pantograph-repl(lean_apply_8+0x2fc) [0xaaaad8c7b140]
/path/to/pantograph/pantograph-repl(l_ReaderT_bind___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__8___rarg+0x114) [0xaaaad53c6ba8]
/path/to/pantograph/pantograph-repl(lean_apply_8+0x45c) [0xaaaad8c7b2a0]
/path/to/pantograph/pantograph-repl(l_Lean_Core_withIncRecDepth___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__9+0x464) [0xaaaad53c7534]
/path/to/pantograph/pantograph-repl(l_Lean_Core_transform_visit___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__4+0xa58) [0xaaaad53c40b4]
/path/to/pantograph/pantograph-repl(l_Lean_Core_transform___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__3+0xfc) [0xaaaad53cee5c]
/path/to/pantograph/pantograph-repl(l___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr+0x1dc) [0xaaaad53d1abc]
/path/to/pantograph/pantograph-repl(l_Pantograph_Frontend_MetaTranslate_translateLocalInstance+0x184) [0xaaaad53d26ec]
/path/to/pantograph/pantograph-repl(l_Array_mapMUnsafe_map___at_Pantograph_Frontend_MetaTranslate_translateMVarId___spec__1+0x19c) [0xaaaad53d20b8]
/path/to/pantograph/pantograph-repl(l_Pantograph_Frontend_MetaTranslate_translateMVarId___lambda__3+0x534) [0xaaaad53d6cd4]
/path/to/pantograph/pantograph-repl(lean_apply_8+0x45c) [0xaaaad8c7b2a0]
/path/to/pantograph/pantograph-repl(lean_apply_5+0x444) [0xaaaad8c79338]
/path/to/pantograph/pantograph-repl(l_Lean_Meta_withLCtx___at_Pantograph_Frontend_MetaTranslate_translateMVarId___spec__6___rarg+0x64) [0xaaaad53d4a2c]
/path/to/pantograph/pantograph-repl(l_Pantograph_Frontend_MetaTranslate_translateMVarId___lambda__4+0x19c) [0xaaaad53d78fc]
/path/to/pantograph/pantograph-repl(l_Pantograph_Frontend_MetaTranslate_translateMVarId+0x564) [0xaaaad53d15f4]
/path/to/pantograph/pantograph-repl(l_List_mapM_loop___at_Pantograph_Frontend_MetaTranslate_translateMVarFromTacticInfoBefore___spec__1+0x274) [0xaaaad53dec94]
/path/to/pantograph/pantograph-repl(l_List_mapM_loop___at_Pantograph_Frontend_sorrysToGoalState___spec__3+0x254) [0xaaaad53f1678]
/path/to/pantograph/pantograph-repl(pantograph_frontend_sorrys_to_goal_state_m+0x1b0) [0xaaaad53f2cb0]
/path/to/pantograph/pantograph-repl(lean_apply_5+0x3ac) [0xaaaad8c792a0]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_runMetaInMainM___rarg+0x88) [0xaaaad5407528]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_runMetaInMainM___rarg___boxed+0x14) [0xaaaad5407c3c]
/path/to/pantograph/pantograph-repl(lean_apply_5+0x3ac) [0xaaaad8c792a0]
/path/to/pantograph/pantograph-repl(l_ReaderT_bind___at_Pantograph_Repl_execute_frontend__process___spec__2___rarg+0x98) [0xaaaad5446a4c]
/path/to/pantograph/pantograph-repl(lean_apply_5+0x3d0) [0xaaaad8c792c4]
/path/to/pantograph/pantograph-repl(l_Lean_withEnv___at_Pantograph_Repl_execute_frontend__process___spec__3+0x1e0) [0xaaaad5446f54]
/path/to/pantograph/pantograph-repl(l_List_mapM_loop___at_Pantograph_Repl_execute_frontend__process___spec__5+0x778) [0xaaaad544923c]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_execute_frontend__process___lambda__5+0x510) [0xaaaad544ac04]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_execute_frontend__process___lambda__7+0x230) [0xaaaad544be84]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_execute_frontend__process+0x180) [0xaaaad544c124]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_execute+0x333c) [0xaaaad54507c8]
/path/to/pantograph/pantograph-repl(l_loop___lambda__2+0x264) [0xaaaad53123fc]
/path/to/pantograph/pantograph-repl(l_loop+0x41c) [0xaaaad53117a0]
/path/to/pantograph/pantograph-repl(l_loop___lambda__1___boxed+0x28) [0xaaaad5313758]
/path/to/pantograph/pantograph-repl(lean_apply_6+0x1f8) [0xaaaad8c79bc0]
/path/to/pantograph/pantograph-repl(l_loop+0x41c) [0xaaaad53117a0]
/path/to/pantograph/pantograph-repl(l_main___lambda__1+0xb4) [0xaaaad5313f60]
/path/to/pantograph/pantograph-repl(l_main___lambda__2+0x554) [0xaaaad5314c6c]
/path/to/pantograph/pantograph-repl(+0xfa61e4) [0xaaaad53161e4]
/usr/lib64/libc.so.6(+0x2b040) [0xffffb93cd040]
/usr/lib64/libc.so.6(__libc_start_main+0x94) [0xffffb93cd118]
/path/to/pantograph/pantograph-repl(_start+0x30) [0xaaaad53104b0]

As the error message suggests, commenting out this line can address the aforementioned JSONDecodeErrors. (However, Unsolved goals remains unsolved):

https://github.com/lenianiva/Pantograph/blob/3744cfaa9608cd43e00078283339662b3720949b/Pantograph/Frontend/MetaTranslate.lean#L71C1-L71C43

I'm still not certain why this assertion fails. Perhaps @lenianiva could conduct a more in-depth inspection.

@lenianiva
Copy link
Member

If this is a problem with Lean's json system we'll have to wait until the upstream is fixed

@lenianiva
Copy link
Member

I can't reproduce the error cases listed here on the upstream head for some reason. Maybe I accidentally fixed it or maybe there's something else going on.

The first one is probably a Python problem

@Purewhite2019 The error is raised by the server, not by json-loading. You can reproduce the error by:

thm = """theorem amc12_2000_p15 (f : ℂ → ℂ) (h₀ : ∀ x, f (x / 3) = x ^ 2 + x + 1)
    (h₁ : Fintype (f ⁻¹' {7})) : (∑ y in (f ⁻¹' {7}).toFinset, y / 3) = -1 / 9 := sorry
"""
unit = server.load_sorry(thm)[0]
Traceback (most recent call last):
  File "/home/cubelab/workspace/Lean/PyPantograph/pantograph/server.py", line 133, in run
    obj = json.loads(line)
  File "/home/cubelab/miniconda3/envs/p2g/lib/python3.10/json/__init__.py", line 346, in loads
    return _default_decoder.decode(s)
  File "/home/cubelab/miniconda3/envs/p2g/lib/python3.10/json/decoder.py", line 337, in decode
    obj, end = self.raw_decode(s, idx=_w(s, 0).end())
  File "/home/cubelab/miniconda3/envs/p2g/lib/python3.10/json/decoder.py", line 355, in raw_decode
    raise JSONDecodeError("Expecting value", s, err.value) from None
json.decoder.JSONDecodeError: Expecting value: line 1 column 1 (char 0)

More precisely, it might be caused by the () in the last condition:

(∑ y in (f ⁻¹' {7}).toFinset, y / 3)

The same applies to the second one. Note that these cases work fine in the Lean Server.

import Mathlib
import Aesop

theorem mathd_numbertheory_552
  (f g h : ℕ+ → ℕ)
  (h₀ : ∀ x, f x = 12 * x + 7)
  (h₁ : ∀ x, g x = 5 * x + 2)
  (h₂ : ∀ x, h x = Nat.gcd (f x) (g x))
  (h₃ : Fintype (Set.range h)) :
  (∑ k in (Set.range h).toFinset, k) = 12 := sorry

theorem amc12_2000_p15 (f : ℂ → ℂ) (h₀ : ∀ x, f (x / 3) = x ^ 2 + x + 1)
    (h₁ : Fintype (f ⁻¹' {7})) : (∑ y in (f ⁻¹' {7}).toFinset, y / 3) = -1 / 9 := sorry

@lenianiva lenianiva added bug Something isn't working help wanted Extra attention is needed labels Jan 9, 2025
@RexWzh
Copy link
Author

RexWzh commented Jan 12, 2025

I can't reproduce the error cases listed here on the upstream head for some reason. Maybe I accidentally fixed it or maybe there's something else going on.

You can check the github action here .

image

Or run pytest -s tests/test_sample.py to reproduce the error.

https://github.com/lenianiva/PyPantograph/blob/affc15a6070e8dee5cb14dd50b460a07f0b395b7/tests/test_sample.py#L48-L56

@RexWzh
Copy link
Author

RexWzh commented Jan 13, 2025 •
edited
Loading

Understood. This does seem rather strange as I've come across several similar issues that were due to json errors and were resolved by setting ensure_ascii=False.

https://github.com/lenianiva/PyPantograph/blob/ee9e70b960d4fb074629fd60976c4675fa2cf27a/pantograph/server.py#L128

This fixes one of the statements:

theorem mathd_algebra_31 (x : NNReal) (u : ℕ → NNReal) (h₀ : ∀ n, u (n + 1) = NNReal.sqrt (x + u n))
    (h₁ : Filter.Tendsto u Filter.atTop (𝓝 9)) : 9 = NNReal.sqrt (x + 9) := by sorry
image

If this is a problem with Lean's json system we'll have to wait until the upstream is fixed

I have tested it in repl and it works.

@Purewhite2019
Copy link

I have tested it in repl and it works.

Exactly. Indeed, this solution was initially designed for the Lean REPL.

@lenianiva
Copy link
Member

I have tested it in repl and it works.

Exactly. Indeed, this solution was initially designed for the Lean REPL.

so that fixes all the issues?

@lenianiva lenianiva mentioned this issue Jan 14, 2025
Merged
@lenianiva
Copy link
Member

The error is raised by the server, not by json-loading. You can reproduce the error by:

Understood. This does seem rather strange as I've come across several similar issues that were due to json errors and were resolved by setting ensure_ascii=False.

I was able to successfully reproduce the error you mentioned. Below is a more detailed error backtrace:

PANIC at _private.Pantograph.Frontend.MetaTranslate.0.Pantograph.Frontend.MetaTranslate.translateExpr Pantograph.Frontend.MetaTranslate:71:6: assertion violation: ( [email protected]._hyg.610.0 ).contains fvarId'

      
backtrace:
/path/to/pantograph/pantograph-repl(lean_panic_fn+0x70) [0xaaaad8c6b250]
/path/to/pantograph/pantograph-repl(l_panic___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__1+0x44) [0xaaaad53c26c4]
/path/to/pantograph/pantograph-repl(lean_apply_7+0x460) [0xaaaad8c7a890]
/path/to/pantograph/pantograph-repl(lean_apply_8+0x2fc) [0xaaaad8c7b140]
/path/to/pantograph/pantograph-repl(l_ReaderT_bind___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__8___rarg+0x114) [0xaaaad53c6ba8]
/path/to/pantograph/pantograph-repl(lean_apply_8+0x45c) [0xaaaad8c7b2a0]
/path/to/pantograph/pantograph-repl(l_Lean_Core_withIncRecDepth___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__9+0x464) [0xaaaad53c7534]
/path/to/pantograph/pantograph-repl(l_Lean_Core_transform_visit___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__4+0xa58) [0xaaaad53c40b4]
/path/to/pantograph/pantograph-repl(l_Lean_Core_transform___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__3+0xfc) [0xaaaad53cee5c]
/path/to/pantograph/pantograph-repl(l___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr+0x1dc) [0xaaaad53d1abc]
/path/to/pantograph/pantograph-repl(l_Pantograph_Frontend_MetaTranslate_translateLocalInstance+0x184) [0xaaaad53d26ec]
/path/to/pantograph/pantograph-repl(l_Array_mapMUnsafe_map___at_Pantograph_Frontend_MetaTranslate_translateMVarId___spec__1+0x19c) [0xaaaad53d20b8]
/path/to/pantograph/pantograph-repl(l_Pantograph_Frontend_MetaTranslate_translateMVarId___lambda__3+0x534) [0xaaaad53d6cd4]
/path/to/pantograph/pantograph-repl(lean_apply_8+0x45c) [0xaaaad8c7b2a0]
/path/to/pantograph/pantograph-repl(lean_apply_5+0x444) [0xaaaad8c79338]
/path/to/pantograph/pantograph-repl(l_Lean_Meta_withLCtx___at_Pantograph_Frontend_MetaTranslate_translateMVarId___spec__6___rarg+0x64) [0xaaaad53d4a2c]
/path/to/pantograph/pantograph-repl(l_Pantograph_Frontend_MetaTranslate_translateMVarId___lambda__4+0x19c) [0xaaaad53d78fc]
/path/to/pantograph/pantograph-repl(l_Pantograph_Frontend_MetaTranslate_translateMVarId+0x564) [0xaaaad53d15f4]
/path/to/pantograph/pantograph-repl(l_List_mapM_loop___at_Pantograph_Frontend_MetaTranslate_translateMVarFromTacticInfoBefore___spec__1+0x274) [0xaaaad53dec94]
/path/to/pantograph/pantograph-repl(l_List_mapM_loop___at_Pantograph_Frontend_sorrysToGoalState___spec__3+0x254) [0xaaaad53f1678]
/path/to/pantograph/pantograph-repl(pantograph_frontend_sorrys_to_goal_state_m+0x1b0) [0xaaaad53f2cb0]
/path/to/pantograph/pantograph-repl(lean_apply_5+0x3ac) [0xaaaad8c792a0]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_runMetaInMainM___rarg+0x88) [0xaaaad5407528]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_runMetaInMainM___rarg___boxed+0x14) [0xaaaad5407c3c]
/path/to/pantograph/pantograph-repl(lean_apply_5+0x3ac) [0xaaaad8c792a0]
/path/to/pantograph/pantograph-repl(l_ReaderT_bind___at_Pantograph_Repl_execute_frontend__process___spec__2___rarg+0x98) [0xaaaad5446a4c]
/path/to/pantograph/pantograph-repl(lean_apply_5+0x3d0) [0xaaaad8c792c4]
/path/to/pantograph/pantograph-repl(l_Lean_withEnv___at_Pantograph_Repl_execute_frontend__process___spec__3+0x1e0) [0xaaaad5446f54]
/path/to/pantograph/pantograph-repl(l_List_mapM_loop___at_Pantograph_Repl_execute_frontend__process___spec__5+0x778) [0xaaaad544923c]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_execute_frontend__process___lambda__5+0x510) [0xaaaad544ac04]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_execute_frontend__process___lambda__7+0x230) [0xaaaad544be84]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_execute_frontend__process+0x180) [0xaaaad544c124]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_execute+0x333c) [0xaaaad54507c8]
/path/to/pantograph/pantograph-repl(l_loop___lambda__2+0x264) [0xaaaad53123fc]
/path/to/pantograph/pantograph-repl(l_loop+0x41c) [0xaaaad53117a0]
/path/to/pantograph/pantograph-repl(l_loop___lambda__1___boxed+0x28) [0xaaaad5313758]
/path/to/pantograph/pantograph-repl(lean_apply_6+0x1f8) [0xaaaad8c79bc0]
/path/to/pantograph/pantograph-repl(l_loop+0x41c) [0xaaaad53117a0]
/path/to/pantograph/pantograph-repl(l_main___lambda__1+0xb4) [0xaaaad5313f60]
/path/to/pantograph/pantograph-repl(l_main___lambda__2+0x554) [0xaaaad5314c6c]
/path/to/pantograph/pantograph-repl(+0xfa61e4) [0xaaaad53161e4]
/usr/lib64/libc.so.6(+0x2b040) [0xffffb93cd040]
/usr/lib64/libc.so.6(__libc_start_main+0x94) [0xffffb93cd118]
/path/to/pantograph/pantograph-repl(_start+0x30) [0xaaaad53104b0]

As the error message suggests, commenting out this line can address the aforementioned JSONDecodeErrors. (However, Unsolved goals remains unsolved):

https://github.com/lenianiva/Pantograph/blob/3744cfaa9608cd43e00078283339662b3720949b/Pantograph/Frontend/MetaTranslate.lean#L71C1-L71C43

I'm still not certain why this assertion fails. Perhaps @lenianiva could conduct a more in-depth inspection.

Does this still occur? I could not trigger it by feeding this into the Pantograph repl:

frontend.process {"file": "theorem amc12_2000_p15 (f : ℂ → ℂ) (h₀ : ∀ x, f (x / 3) = x ^ 2 + x + 1) (h₁ : Fintype (f ⁻¹' {7})) : (∑ y in (f ⁻¹' {7}).toFinset, y / 3) = -1 / 9 := sorry", "invocations": false, "sorrys": true, "newConstants": false, "typeErrorsAsGoals": false }

and it outputs

⮀ lake env ~/Projects/atp/PyPantograph/pantograph/pantograph-repl Mathlib < pantograph-test/amc12_2020_p15.jsonl
ready.
{"units":[{"messages":["<anonymous>:1:8: warning: declaration uses 'sorry'\n"],"goals":[{"vars":[{"userName":"f","type":{"pp":"ℂ → ℂ"},"name":"_uniq.12","isInaccessible":false},{"userName":"h₀","type":{"pp":"∀ (x : ℂ), f (x / 3) = x ^ 2 + x + 1"},"name":"_uniq.14","isInaccessible":false},{"userName":"h₁","type":{"pp":"Fintype ↑(f ⁻¹' {7})"},"name":"_uniq.16","isInaccessible":false}],"target":{"pp":"∑ y ∈ (f ⁻¹' {7}).toFinset, y / 3 = -1 / 9"},"name":"_uniq.18","isConversion":false}],"goalStateId":0,"goalSrcBoundaries":[[171,176]],"boundary":[0,176]}]}

which is successful. I've been chasing down this mysterious bug for days and I could not reproduce it.

@Purewhite2019
Copy link

I could not trigger it by feeding this into the Pantograph repl:

frontend.process {"file": "theorem amc12_2000_p15 (f : ℂ → ℂ) (h₀ : ∀ x, f (x / 3) = x ^ 2 + x + 1) (h₁ : Fintype (f ⁻¹' {7})) : (∑ y in (f ⁻¹' {7}).toFinset, y / 3) = -1 / 9 := sorry", "invocations": false, "sorrys": true, "newConstants": false, "typeErrorsAsGoals": false }

Please try this

frontend.process {"file": "theorem amc12_2000_p15 (f : ℂ → ℂ) (h₀ : ∀ x, f (x / 3) = x ^ 2 + x + 1)\n    (h₁ : Fintype (f ⁻¹' {7})) : (∑ y in (f ⁻¹' {7}).toFinset, y / 3) = -1 / 9 := by sorry", "invocations": false, "sorrys": true, "newConstants": false, "typeErrorsAsGoals": false}

When using by sorry instead of sorry, the following error occurs

PANIC at _private.Pantograph.Frontend.MetaTranslate.0.Pantograph.Frontend.MetaTranslate.translateExpr Pantograph.Frontend.MetaTranslate:71:6: assertion violation: ( [email protected]._hyg.610.0 ).contains fvarId'
      
backtrace:
/path/to/pantograph/pantograph-repl(lean_panic_fn+0x70) [0xaaaae0bfdc58]
/path/to/pantograph/pantograph-repl(l_panic___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__1+0x44) [0xaaaadd354d70]
/path/to/pantograph/pantograph-repl(lean_apply_7+0x460) [0xaaaae0c0d298]
/path/to/pantograph/pantograph-repl(lean_apply_8+0x2fc) [0xaaaae0c0db48]
/path/to/pantograph/pantograph-repl(l_ReaderT_bind___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__8___rarg+0x114) [0xaaaadd359254]
/path/to/pantograph/pantograph-repl(lean_apply_8+0x45c) [0xaaaae0c0dca8]
/path/to/pantograph/pantograph-repl(l_Lean_Core_withIncRecDepth___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__9+0x464) [0xaaaadd359be0]
/path/to/pantograph/pantograph-repl(l_Lean_Core_transform_visit___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__4+0xa58) [0xaaaadd356760]
/path/to/pantograph/pantograph-repl(l_Lean_Core_transform___at___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr___spec__3+0xfc) [0xaaaadd361508]
/path/to/pantograph/pantograph-repl(l___private_Pantograph_Frontend_MetaTranslate_0__Pantograph_Frontend_MetaTranslate_translateExpr+0x1dc) [0xaaaadd364168]
/path/to/pantograph/pantograph-repl(l_Pantograph_Frontend_MetaTranslate_translateLocalInstance+0x184) [0xaaaadd364d98]
/path/to/pantograph/pantograph-repl(l_Array_mapMUnsafe_map___at_Pantograph_Frontend_MetaTranslate_translateMVarId___spec__1+0x19c) [0xaaaadd364764]
/path/to/pantograph/pantograph-repl(l_Pantograph_Frontend_MetaTranslate_translateMVarId___lambda__3+0x534) [0xaaaadd369380]
/path/to/pantograph/pantograph-repl(lean_apply_8+0x45c) [0xaaaae0c0dca8]
/path/to/pantograph/pantograph-repl(lean_apply_5+0x444) [0xaaaae0c0bd40]
/path/to/pantograph/pantograph-repl(l_Lean_Meta_withLCtx___at_Pantograph_Frontend_MetaTranslate_translateMVarId___spec__6___rarg+0x64) [0xaaaadd3670d8]
/path/to/pantograph/pantograph-repl(l_Pantograph_Frontend_MetaTranslate_translateMVarId___lambda__4+0x19c) [0xaaaadd369fa8]
/path/to/pantograph/pantograph-repl(l_Pantograph_Frontend_MetaTranslate_translateMVarId+0x564) [0xaaaadd363ca0]
/path/to/pantograph/pantograph-repl(l_List_mapM_loop___at_Pantograph_Frontend_MetaTranslate_translateMVarFromTacticInfoBefore___spec__1+0x274) [0xaaaadd371340]
/path/to/pantograph/pantograph-repl(l_List_mapM_loop___at_Pantograph_Frontend_sorrysToGoalState___spec__3+0x254) [0xaaaadd384090]
/path/to/pantograph/pantograph-repl(pantograph_frontend_sorrys_to_goal_state_m+0x1b0) [0xaaaadd3856c8]
/path/to/pantograph/pantograph-repl(lean_apply_5+0x3ac) [0xaaaae0c0bca8]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_runMetaInMainM___rarg+0x88) [0xaaaadd399f24]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_runMetaInMainM___rarg___boxed+0x14) [0xaaaadd39a638]
/path/to/pantograph/pantograph-repl(lean_apply_5+0x3ac) [0xaaaae0c0bca8]
/path/to/pantograph/pantograph-repl(l_ReaderT_bind___at_Pantograph_Repl_execute_frontend__process___spec__2___rarg+0x98) [0xaaaadd3d9448]
/path/to/pantograph/pantograph-repl(lean_apply_5+0x3d0) [0xaaaae0c0bccc]
/path/to/pantograph/pantograph-repl(l_Lean_withEnv___at_Pantograph_Repl_execute_frontend__process___spec__3+0x1e0) [0xaaaadd3d9950]
/path/to/pantograph/pantograph-repl(l_List_mapM_loop___at_Pantograph_Repl_execute_frontend__process___spec__5+0x778) [0xaaaadd3dbc38]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_execute_frontend__process___lambda__5+0x510) [0xaaaadd3dd60c]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_execute_frontend__process___lambda__7+0x230) [0xaaaadd3de88c]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_execute_frontend__process+0x180) [0xaaaadd3deb2c]
/path/to/pantograph/pantograph-repl(l_Pantograph_Repl_execute+0x333c) [0xaaaadd3e31d0]
/path/to/pantograph/pantograph-repl(l_loop___lambda__2+0x264) [0xaaaadd2a3460]
/path/to/pantograph/pantograph-repl(l_loop+0x428) [0xaaaadd2a2bd0]
/path/to/pantograph/pantograph-repl(l_main___lambda__1+0xb4) [0xaaaadd2a517c]
/path/to/pantograph/pantograph-repl(l_main___lambda__2+0x554) [0xaaaadd2a5e88]
/path/to/pantograph/pantograph-repl(+0xfa7400) [0xaaaadd2a7400]
/usr/lib64/libc.so.6(+0x2b040) [0xffffa7934040]
/usr/lib64/libc.so.6(__libc_start_main+0x94) [0xffffa7934118]
/path/to/pantograph/pantograph-repl(_start+0x30) [0xaaaadd2a0ab0]
{"units":[{"messages":["<anonymous>:1:8: warning: declaration uses 'sorry'\n"],"goals":[{"vars":[{"userName":"f","type":{"pp":"ℂ → ℂ"},"name":"_uniq.12","isInaccessible":false},{"userName":"h₀","type":{"pp":"∀ (x : ℂ), f (x / 3) = x ^ 2 + x + 1"},"name":"_uniq.14","isInaccessible":false},{"userName":"h₁","type":{"pp":"Fintype ↑(f ⁻¹' {7})"},"name":"_uniq.16","isInaccessible":false}],"target":{"pp":"∑ y ∈ (f ⁻¹' {7}).toFinset, y / 3 = -1 / 9"},"name":"_uniq.18","isConversion":false}],"goalStateId":0,"goalSrcBoundaries":[[178,183]],"boundary":[0,183]}]}

Maybe it originates from the distinct behavior of the sorry tactic (Lean.Parser.Tactic.tacticSorry) and the sorry term?

@lenianiva
Copy link
Member

Would it be an acceptable solution to remove most of the drafting features (:= sorry will remain) from frontend.process and implement them using the new draft tactic? It is more versatile and requires less hacking into Lean, so it should be more resistant to edge cases like this.

@lenianiva
Copy link
Member

I've removed the over-eager assertion failure on the upstream branch here:

https://git.leni.sh/aniva/Pantograph/pulls/158

Moving forward, I will probably deprecate tactic-based drafting in load_sorry, so instead of

example : ... := by
  have a : A := sorry
  sorry

you can write

example : ... := sorry

and use the new draft tactic with this draft

by
have a : A := sorry
sorry

which is more robust, and allows for recursive drafting.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug Something isn't working help wanted Extra attention is needed
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@Purewhite2019 @RexWzh @lenianiva