chore: bump to 2022-08-31

[gebner]

Fixes #158.

[gebner]

Broke because of AST changes in Lean 3.47

[gebner]

Ok, there's lots of errors.

--- mathport name: «expr ⁺»
+-- mathport name: ««expr ⁺»»

-protected theorem map_sum {ι : Type _} (f : ι → A) (s : Finset ι) : φ (∑ x in s, f x) = ∑ x in s, φ (f x) :=
+-- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `finset.sum
+-- ./././Mathport/Syntax/Translate/Expr.lean:210:13: unsupported notation `finset.sum
+-- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `finset.sum
+-- ./././Mathport/Syntax/Translate/Expr.lean:210:13: unsupported notation `finset.sum
+protected theorem map_sum {ι : Type _} (f : ι → A) (s : Finset ι) :
+    φ (finset.sum "./././Mathport/Syntax/Translate/Expr.lean:210:13: unsupported notation `finset.sum" s (f x)) =
+      finset.sum "./././Mathport/Syntax/Translate/Expr.lean:210:13: unsupported notation `finset.sum" s (φ (f x)) :=

There's some other notation name errors as well but they are probably related to the finset.sum stuff.

+-- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation
+-- ./././Mathport/Syntax/Translate/Expr.lean:207:4: warning: unsupported notation `finset.product
 /-- The product of two vector bundles is a vector bundle. -/
 instance _root_.bundle.prod.topological_vector_bundle : TopologicalVectorBundle R (F₁ × F₂) (E₁×ᵇE₂) where

[digama0]

The mathport name: ««expr ⁺»» issue is trivial to fix (the printout was just adding the «» itself).

I'm not sure what's wrong with the finset.sum notation.

The last error is probably legitimate: it was an ambiguous notation before (a choice node) but both notations had the same name so we just went with one of them and hoped for the best. Now we can tell that they are different and give the error, but I think we could revert to the "hope for the best" behavior since I don't think we have any better plan for how to refer to an ambiguous notation.

[digama0]

I think the finset.sum issue was caused by an errant getString! being used on a nonatomic name (specifically, finset.sum), a previously impossible situation (since heuristic names are always simple). So the first two error types should hopefully be fixed now, but I expect the "ambiguous notation" error to persist.

[gebner]

This is what I like to see!

--- ./././Mathport/Syntax/Translate/Expr.lean:194:47: unsupported (impossible)
--- ./././Mathport/Syntax/Translate/Expr.lean:194:47: unsupported (impossible)
--- ./././Mathport/Syntax/Translate/Expr.lean:194:47: unsupported (impossible)
--- ./././Mathport/Syntax/Translate/Expr.lean:194:47: unsupported (impossible)
-theorem image_interval_eq_Icc
-    (h : ContinuousOn f <| "./././Mathport/Syntax/Translate/Expr.lean:194:47: unsupported (impossible)") :
-    f '' "./././Mathport/Syntax/Translate/Expr.lean:194:47: unsupported (impossible)" =
-      Icc (inf (f '' "./././Mathport/Syntax/Translate/Expr.lean:194:47: unsupported (impossible)"))
-        (sup (f '' "./././Mathport/Syntax/Translate/Expr.lean:194:47: unsupported (impossible)")) :=
-  by
+theorem image_interval_eq_Icc (h : ContinuousOn f <| [a, b]) :
+    f '' [a, b] = Icc (inf (f '' [a, b])) (sup (f '' [a, b])) := by