-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathholonomic_fix.txt
More file actions
120 lines (108 loc) · 16.4 KB
/
Copy pathholonomic_fix.txt
File metadata and controls
120 lines (108 loc) · 16.4 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
lake : warning: UnicodeBasic: repository
'C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake/packages\UnicodeBasic' has local changes
In C:\Users\fabi0\AppData\Local\Temp\ps-script-41d2c879-7583-4caf-940d-462a5076981a.ps1:135 Zeichen:61
+ ... ty\joyful-lavoisier"; lake build ISAR.HolonomicInstances 2>&1 | Tee-O ...
+ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+ CategoryInfo : NotSpecified: (warning: Unicod...s local changes:String) [], RemoteException
+ FullyQualifiedErrorId : NativeCommandError
ÔÜá [3061/3068] Replayed ISAR.Holonomic
warning: src/ISAR/Holonomic.lean:90:15: This simp argument is unused:
Fin.val_mk
Hint: Omit it from the simp argument list.
simp only [F╠Ái╠Án╠Á.╠Áv╠Áa╠Ál╠Á_╠Ám╠Ák╠Á,╠Á ╠Áhne, ÔåôreduceDIte]
Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
Ô£û [3068/3068] Building ISAR.HolonomicInstances (139s)
trace: .> LEAN_PATH=C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\batteries\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\Qq\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\aesop\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\proofwidgets\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\importGraph\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\LeanSearchClient\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\plausible\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\MD4Lean\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\BibtexQuery\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\UnicodeBasic\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\Cli\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\leansqlite\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\mathlib\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\checkdecls\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\packages\doc-gen4\.lake\build\lib\lean;C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\build\lib\lean c:\Users\fabi0\.elan\toolchains\leanprover--lean4---v4.31.0\bin\lean.exe C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\src\ISAR\HolonomicInstances.lean -o C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\build\lib\lean\ISAR\HolonomicInstances.olean -i C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\build\lib\lean\ISAR\HolonomicInstances.ilean -c C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\build\ir\ISAR\HolonomicInstances.c --setup C:\Users\fabi0\Documents\antigravity\joyful-lavoisier\.lake\build\ir\ISAR\HolonomicInstances.setup.json --json
error: src/ISAR/HolonomicInstances.lean:173:4: No applicable extensionality theorem found for type
AddCommGroup 
Note: Extensionality theorems can be registered by marking them with the `[ext]` attribute
error: src/ISAR/HolonomicInstances.lean:174:4: `ring_nf` made no progress on the goal
error: src/ISAR/HolonomicInstances.lean:171:49: unsolved goals
case e'_8
x : 
 (fun y  -(2 * y)) = -fun y  2 * id y
case e'_9
x : 
Ôèó -2 = -(2 * 1)
error: src/ISAR/HolonomicInstances.lean:183:4: No applicable extensionality theorem found for type
AddCommGroup 
Note: Extensionality theorems can be registered by marking them with the `[ext]` attribute
error: src/ISAR/HolonomicInstances.lean:184:4: `ring_nf` made no progress on the goal
error: src/ISAR/HolonomicInstances.lean:178:76: unsolved goals
case e'_8
x : 
heq : deriv gaussian = fun y  gaussian y * -(2 * y)
 (fun y  gaussian y * -(2 * y)) = gaussian * fun y  -(2 * y)
case e'_9
x : 
heq : deriv gaussian = fun y  gaussian y * -(2 * y)
Ôèó -2 * gaussian x + gaussian x * -(2 * x) * -(2 * x) = gaussian x * -(2 * x) * -(2 * x) + gaussian x * -2
error: src/ISAR/HolonomicInstances.lean:217:6: No applicable extensionality theorem found for type

Note: Extensionality theorems can be registered by marking them with the `[ext]` attribute
error: src/ISAR/HolonomicInstances.lean:221:4: No goals to be solved
error: src/ISAR/HolonomicInstances.lean:246:2: No goals to be solved
error: src/ISAR/HolonomicInstances.lean:275:8: No applicable extensionality theorem found for type
AddCommGroup 
Note: Extensionality theorems can be registered by marking them with the `[ext]` attribute
error: src/ISAR/HolonomicInstances.lean:276:8: `ring_nf` made no progress on the goal
error: src/ISAR/HolonomicInstances.lean:271:78: unsolved goals
case e'_8
x : 
h1 : deriv (fresnelSin * gaussian) x = Real.cos (x ^ 2) * (2 * x) * gaussian x + fresnelSin x * (gaussian x * -(2 * x))
heq :
deriv (fresnelSin * gaussian) = fun y 
Real.cos (y ^ 2) * (2 * y) * gaussian y + fresnelSin y * (gaussian y * -(2 * y))
hlin : HasDerivAt (fun y  2 * y) 2 x
 (fun y  Real.cos (y ^ 2) * (2 * y)) = (fun x  Real.cos (x ^ 2)) * fun y  2 * y
error: src/ISAR/HolonomicInstances.lean:278:6: No applicable extensionality theorem found for type
AddCommGroup 
Note: Extensionality theorems can be registered by marking them with the `[ext]` attribute
error: src/ISAR/HolonomicInstances.lean:279:6: `ring_nf` made no progress on the goal
error: src/ISAR/HolonomicInstances.lean:269:69: unsolved goals
case e'_8
x : 
h1 : deriv (fresnelSin * gaussian) x = Real.cos (x ^ 2) * (2 * x) * gaussian x + fresnelSin x * (gaussian x * -(2 * x))
heq :
deriv (fresnelSin * gaussian) = fun y 
Real.cos (y ^ 2) * (2 * y) * gaussian y + fresnelSin y * (gaussian y * -(2 * y))
hcg : HasDerivAt (fun y  Real.cos (y ^ 2) * (2 * y)) (-Real.sin (x ^ 2) * (2 * x) * (2 * x) + Real.cos (x ^ 2) * 2) x
 (fun y  Real.cos (y ^ 2) * (2 * y) * gaussian y) = (fun y  Real.cos (y ^ 2) * (2 * y)) * gaussian
error: src/ISAR/HolonomicInstances.lean:287:6: No applicable extensionality theorem found for type
AddCommGroup 
Note: Extensionality theorems can be registered by marking them with the `[ext]` attribute
error: src/ISAR/HolonomicInstances.lean:288:6: `simp` made no progress
error: src/ISAR/HolonomicInstances.lean:284:81: unsolved goals
case e'_8
x : 
h1 : deriv (fresnelSin * gaussian) x = Real.cos (x ^ 2) * (2 * x) * gaussian x + fresnelSin x * (gaussian x * -(2 * x))
heq :
deriv (fresnelSin * gaussian) = fun y 
Real.cos (y ^ 2) * (2 * y) * gaussian y + fresnelSin y * (gaussian y * -(2 * y))
hleft :
HasDerivAt (fun y  Real.cos (y ^ 2) * (2 * y) * gaussian y)
((-Real.sin (x ^ 2) * (2 * x) * (2 * x) + Real.cos (x ^ 2) * 2) * gaussian x +
Real.cos (x ^ 2) * (2 * x) * (gaussian x * -(2 * x)))
x
hrate : HasDerivAt (gaussian * fun y  -(2 * y)) (gaussian x * -(2 * x) * -(2 * x) + gaussian x * -2) x
 (fun y  fresnelSin y * (gaussian y * -(2 * y))) = fresnelSin * (gaussian * fun y  -(2 * y))
case e'_9
x : 
h1 : deriv (fresnelSin * gaussian) x = Real.cos (x ^ 2) * (2 * x) * gaussian x + fresnelSin x * (gaussian x * -(2 * x))
heq :
deriv (fresnelSin * gaussian) = fun y 
Real.cos (y ^ 2) * (2 * y) * gaussian y + fresnelSin y * (gaussian y * -(2 * y))
hleft :
HasDerivAt (fun y  Real.cos (y ^ 2) * (2 * y) * gaussian y)
((-Real.sin (x ^ 2) * (2 * x) * (2 * x) + Real.cos (x ^ 2) * 2) * gaussian x +
Real.cos (x ^ 2) * (2 * x) * (gaussian x * -(2 * x)))
x
hrate : HasDerivAt (gaussian * fun y  -(2 * y)) (gaussian x * -(2 * x) * -(2 * x) + gaussian x * -2) x
Ôèó Real.cos (x ^ 2) * (2 * x) * (gaussian x * -(2 * x)) +
fresnelSin x * (-2 * gaussian x + gaussian x * -(2 * x) * -(2 * x)) =
Real.cos (x ^ 2) * (2 * x) * (gaussian * fun y  -(2 * y)) x +
fresnelSin x * (gaussian x * -(2 * x) * -(2 * x) + gaussian x * -2)
error: Lean exited with code 1
Some required targets logged failures:
- ISAR.HolonomicInstances
error: build failed