Skip to content
This repository has been archived by the owner on Oct 14, 2023. It is now read-only.

update cross-compiler for windows (MXE) to use latest gcc-4.8 snapshot and test thread_local support Edit #7

Closed
soonhokong opened this issue Dec 6, 2013 · 1 comment
Closed

update cross-compiler for windows (MXE) to use latest gcc-4.8 snapshot and test thread_local support Edit #7

soonhokong opened this issue Dec 6, 2013 · 1 comment
Assignees
@soonhokong
Labels
bug

Comments

@soonhokong
Copy link
Contributor

Problem

Using x86_64-w64-mingw32-g++ (GCC) 4.8.2 and cross compiling on Linux, Lean is crashing when a thread access thread_local storage.

Reference: http://stackoverflow.com/questions/20277625/why-does-this-usage-of-thread-local-crash?noredirect=1#comment30423002_20277625

Possible Fix

Use the latest snapshot of gcc-4.8 in MXE.
@ghost ghost assigned soonhokong Dec 6, 2013
@soonhokong
Copy link
Contributor Author

See commit @64963bd9fb05698fa359e3639e565b5c9979ba90

  • To cross-compile windows build on Linux, we use a new version of gcc-4.8.3, snapshot: 20131205.
  • The build environment (pre-compiled cross-compiler/libraries, MXE) is available at here.
  • You can also find the detailed instruction on how to use MXE at here .

leodemoura added a commit that referenced this issue Dec 15, 2013
@leodemoura
feat(library/elaborator): provide the metavar_env to instantiate and …
160a837 
…lift_free_vars in the elaborator, it will minimize the number of local_entries needed

The modifications started at commit 1852c86 made a big difference. For example, before these changes test tests/lean/implicit7.lean generated complicated constraints such as:

[x : Type; a : ?M::29[inst:1 ?M::0[lift:0:1]] x] ⊢ Pi B : Type, (Pi _ : x, (Pi _ : (?M::35[inst:0 #0, inst:1 #2, inst:2 #4, inst:3 #6, inst:5 #5, inst:6 #7, inst:7 #9, inst:9 #9, inst:10 #11, inst:13 ?M::0[lift:0:13]] x a B _), (?M::36[inst:1 #1, inst:2 #3, inst:3 #5, inst:4 #7, inst:6 #6, inst:7 #8, inst:8 #10, inst:10 #10, inst:11 #12, inst:14 ?M::0[lift:0:14]] x a B _ _))) ≈
?M::22 x a

After the changes, only very simple constraints are generated. The most complicated one is:

[] ⊢ Pi a : ?M::0, (Pi B : Type, (Pi _ : ?M::0, (Pi _ : B, ?M::0))) ≈ Pi x : ?M::17, ?M::18

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
khoek pushed a commit to khoek/klean that referenced this issue Apr 10, 2019
@cipher1024
fix(vm/get_cwd): add test for get_cwd (leanprover#7)
1674995
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees

@soonhokong soonhokong

Labels
bug
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@soonhokong