Panic in Mathport

Stream: lean4

[Bhavik Mehta]

I'm getting this error in porting a large project.

PANIC at Mathport.Parse.decodeDecimal! Mathport.Syntax.Parse:163:9: decodeDecimal! failed

The last statement that's mentioned in the mathport output is:

lemma claim_a4 {x y : ℝ} (hx : x ∈ Icc (0.75 : ℝ) 1) (hy : y ∈ Icc (0 : ℝ) 0.75)
  (h : x = 3 / 5 * y + 0.5454) :
  f2 x y < 1.9993 :=

[Bhavik Mehta]

Also, in the meantime, should I try to fix the other porting errors that I've got or should I wait until this one gets resolved somehow

[Mario Carneiro]

that's a new one, although I can understand why, mathlib isn't big on... numbers

[Mario Carneiro]

It would help if you could make a MWE which reproduces in oneshot

[Mario Carneiro]

(it's fine to depend on mathlib if necessary)

[Bhavik Mehta]

This is maybe a silly question, but my mathport folder is currently set up to port a project, can I just follow the oneshot instructions as written or should I delete some stuff (like the output oleans)

[Mario Carneiro]

they don't interfere with each other, you mostly just have a leg up for running oneshot (having done all the setup steps) and make oneshot should just work

[Bhavik Mehta]

I'm trying to make a MWE at the moment, my first two guesses at what would break it weren't correct so I'll post the proof here:

lemma claim_a4 {x y : ℝ} (hx : x ∈ Icc (0.75 : ℝ) 1) (hy : y ∈ Icc (0 : ℝ) 0.75)
  (h : x = 3 / 5 * y + 0.5454) :
  f2 x y < 1.9993 :=
begin
  have hx09 : x ≤ 0.9954 := by linarith only [h, hy.2],
  have hx1 : x < 1 := hx09.trans_lt (by norm_num1),
  have hx2 : x ≠ 2 := by linarith only [hx1],
  rw [f2, f_inner_eq h, ←important_rewrite hx2, ←f2'],
  exact claim_a4_aux ⟨hx.1, hx1⟩,
end

Since it seems to be a parsing issue I figured that the problem would need to be in hx09 or the statement, but using just those wasn't good enough... I'll keep trying, but is there anything here that stands out as problematic that I should focus on?

[Mario Carneiro]

what are the imports?

[Bhavik Mehta]

This isn't my MWE!

[Mario Carneiro]

I mean, if the imports are wrong then lean 3 will fail to parse it and mathport will have a much worse time

[Mario Carneiro]

I got this to parse:

import data.real.basic
import data.set.intervals.basic
open set
def f2 : ℝ → ℝ → ℝ := sorry
lemma claim_a4 {x y : ℝ} (hx : x ∈ Icc (0.75 : ℝ) 1) (hy : y ∈ Icc (0 : ℝ) 0.75)
  (h : x = 3 / 5 * y + 0.5454) :
  f2 x y < 1.9993 :=
sorry

[Bhavik Mehta]

Yeah me too, but that doesn't panic mathport

[Mario Carneiro]

Could you send the .ast.json file corresponding to this example?

[Bhavik Mehta]

import Data.Real.Basic

open set

def f2 (x y : ℝ) := x + y

lemma claim_a4 {x y : ℝ} (hx : x ∈ Icc (0.75 : ℝ) 1) (hy : y ∈ Icc (0 : ℝ) 0.75)
  (h : x = 3 / 5 * y + 0.5454) :
  f2 x y < 1.9993 :=
begin
  have hx09 : x ≤ 0.9954 := by linarith only [h, hy.2],
  have hx1 : x < 1 := hx09.trans_lt (by norm_num1),
  have hx2 : x ≠ 2 := by linarith only [hx1],
  rw [f2],
  linarith
end

this is fine for mathport too - it doesn't throw a panic, but unfortunately I have about 18k lines of code before this so minimising by cutting might be tricky

[Bhavik Mehta]

Mario Carneiro said:

Could you send the .ast.json file corresponding to this example?

I tried opening it in nvim and it had close to a million tokens...

[Mario Carneiro]

just attach the file here

[Mario Carneiro]

re: minimizing, putting sorry in proofs should be fine and presumably really cuts down on the file size

[Bhavik Mehta]

necessary_log_estimates.ast.json

[Bhavik Mehta]

Mario Carneiro said:

re: minimizing, putting sorry in proofs should be fine and presumably really cuts down on the file size

Alright, good to know I can sorry things for mathport

[Mario Carneiro]

Aha, there is a decimal with value 0 at line 822, char 48

[Mario Carneiro]

what does that line look like?

[Bhavik Mehta]

lemma g_deriv_eval_max : g'_deriv 0.4339 ∈ Icc (0.000000 : ℝ) 0.000001 :=

[Bhavik Mehta]

indeed, there is a decimal with value 0

[Mario Carneiro]

mathport's like "why aren't you just writing 0 then?"

[Bhavik Mehta]

(in my defense I think it was 0.0000006 earlier, and I changed it)

[Bhavik Mehta]

That makes sense, although the error location was confusing! Is there something more efficient I should do now (after just writing 0) or should I just run mathport from scratch on the whole project

[Mario Carneiro]

It's a mathport bug, it should be able to handle this kind of decimal literal of course

[Mario Carneiro]

I would guess that 1.0 also causes the panic

[Bhavik Mehta]

I don't imagine it'll get hit very often in fairness! (except by me, 24 lines later)

[Mario Carneiro]

pushed a fix

[Bhavik Mehta]

Thanks so much! Do I need to make the ast/tlean stuff for the whole project again or can I just do it for this file and the ones below it? And similarly for running mathport itself (there's two files below this one and many above)

[Mario Carneiro]

just this file

[Bhavik Mehta]

Great, and I can do mathport oneshot for this file too?

[Mario Carneiro]

you should be able to git pull, lake build and use the existing release data

[Mario Carneiro]

I'm not sure what you mean by that question

[Bhavik Mehta]

I've done lean --make --recursive --ast --tlean for this file, do I now run ./build/bin/mathport --make config-project.json Project::all, or is there some shortcut so I don't need to run mathport on the entire project?

[Mario Carneiro]

I think mathport --make should automatically skip files that have already been done

[Mario Carneiro]

you don't need to rerun lean --ast --tlean

[Bhavik Mehta]

Oh! I misunderstood, alright

[Bhavik Mehta]

Worked great, thank you