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.

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

Segmentation fault error #31

Open
ayush1801 opened this issue Feb 6, 2023 · 0 comments
Open

Segmentation fault error #31

ayush1801 opened this issue Feb 6, 2023 · 0 comments

Comments

@ayush1801
Copy link

I am getting segmentation fault error after trying the following:

["init_search",["one_div_add_one_div","set"]]
{"error":null,"proof_steps":[],"search_id":"0","tactic_state":"⊢ ∀ {K : Type u} [_inst_1 : field K] {a b : K}, a ≠ 0 → b ≠ 0 → 1 / a + 1 / b = (a + b) / (a * b)","tactic_state_id":"0"}
["run_tac",["0","0","intros"]]
{"error":null,"proof_steps":[],"search_id":"0","tactic_state":"K : Type u,\n_inst_1 : field K,\na b : K,\nha : a ≠ 0,\nhb : b ≠ 0\n⊢ 1 / a + 1 / b = (a + b) / (a * b)","tactic_state_id":"1"}
["run_tac",["0","1","rw one_div"]]
{"error":null,"proof_steps":[],"search_id":"0","tactic_state":"K : Type u,\n_inst_1 : field K,\na b : K,\nha : a ≠ 0,\nhb : b ≠ 0\n⊢ a⁻¹ + 1 / b = (a + b) / (a * b)","tactic_state_id":"2"}
["run_tac",["0","2","simp [div_eq_mul_inv, inv_eq_one_div]"]]
Segmentation fault (core dumped)

However, on another machine, this was the output (timeout!):

["init_search",["one_div_add_one_div","set"]]
{"error":null,"proof_steps":[],"search_id":"0","tactic_state":"⊢ ∀ {K : Type u} [_inst_1 : field K] {a b : K}, a ≠ 0 → b ≠ 0 → 1 / a + 1 / b = (a + b) / (a * b)","tactic_state_id":"0"}
["run_tac",["0","0","intros"]]
{"error":null,"proof_steps":[],"search_id":"0","tactic_state":"K : Type u,\n_inst_1 : field K,\na b : K,\nha : a ≠ 0,\nhb : b ≠ 0\n⊢ 1 / a + 1 / b = (a + b) / (a * b)","tactic_state_id":"1"}
["run_tac",["0","1","rw one_div"]]
{"error":null,"proof_steps":[],"search_id":"0","tactic_state":"K : Type u,\n_inst_1 : field K,\na b : K,\nha : a ≠ 0,\nhb : b ≠ 0\n⊢ a⁻¹ + 1 / b = (a + b) / (a * b)","tactic_state_id":"2"}
["run_tac",["0","2","simp [div_eq_mul_inv, inv_eq_one_div]"]]
{"error":"gen_tac_and_capture_res_failed: pos=none msg=try_for tactic failed, timeout","proof_steps":[],"search_id":null,"tactic_state":null,"tactic_state_id":null}

Lean versions used are the same in both the machines: Lean (version 3.39.1, commit 1781ded0d006, Release)

Any idea of what I might be missing?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant