@Kha I marked the corresponding methods as `protected`.
I currently can't stand `throw_error`, and I am optimistic about
server highlighting feature you are working on :)
@Kha This is a hack to try to fix the build.
It seems it is the circular dependency issue again.
Remarks:
- The problem doesn't happen on my Mac.
- I managed to reproduce the Linux error on a virtual machine.
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_ShareCommonT_monadShareCommon___rarg':
ShareCommon.c:(.text+0xc9): undefined reference to `lean_state_sharecommon'
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_PShareCommonT_monadShareCommon___rarg':
ShareCommon.c:(.text+0x259): undefined reference to `lean_persistent_state_sharecommon'
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_ShareCommon_Object_hash___boxed':
ShareCommon.c:(.text+0x59a): undefined reference to `lean_sharecommon_hash'
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_shareCommon___rarg':
ShareCommon.c:(.text+0x6cf): undefined reference to `lean_state_sharecommon'
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_ShareCommon_Object_eq___boxed':
ShareCommon.c:(.text+0x82d): undefined reference to `lean_sharecommon_eq'
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_PShareCommonT_withShareCommon___rarg':
ShareCommon.c:(.text+0x956): undefined reference to `lean_persistent_state_sharecommon'
/usr/bin/ld: ../lib/lean/libStd.a(ShareCommon.o): in function `l_Std_ShareCommonT_withShareCommon___rarg':
ShareCommon.c:(.text+0xae6): undefined reference to `lean_state_sharecommon'
/
@Kha This is a performance bottleneck in a several benchmarks that
create huge proofs. It may negatively affect other files.
I will keep an eye at the speedcenter.
This issue exposed two bugs at `Structural.lean`
1- `getFixedPrefix` was using structural equality to detected fixed
arguments. We should use definitional equality.
2- The `replaceFVars` was broken. We should use `instantiateForall` instead.
@Kha I was tired of writing `arbitrary _` :)
There 0 places in the stdlib where the type needs to be provided.
If in the future we need to specify the type we can use
`arbitrary (α := <type>)`
@Kha I implemented the optional `,` at structure instances.
You have suggested it a few weeks/months ago. F# also implements this
feature. I got back to it while write documentation for Lean.
It looks quite nice when we are packing many functions into a structure.
BTW, F# also has optional separators for list literals :)
This is a much simpler change for us since `[...]` is defined using
the `syntax/macro_rules` commands, but I didn't find optional ','
would very useful since our list literals are usually in a single
line.
`Structural.lean` uses `mkAppM` for creating projections `PProd.fst`
and `PProd.snd`. However, given `x : (([Decidable p] → Bool) × Nat`,
the old ``mkApp `PProd.fst #[x]`` returned
```
Prod.fst ([Decidable p] → Bool) Nat x _inst
```
The extra unexpected argument `_inst` broke `Structural.lean`.
In the new implementation, it returns
```
Prod.fst ([Decidable p] → Bool) Nat x
```
which has type `[Decidable p] → Bool`.
