This repository has been frozen. Lean 4 is now the official release.
Stable and nightly binary releases of Lean are available on the homepage. For building Lean from source, see the build instructions.
Lean Theorem Prover
Home Page: http://leanprover.github.io/
License: Apache License 2.0
This repository has been frozen. Lean 4 is now the official release.
Stable and nightly binary releases of Lean are available on the homepage. For building Lean from source, see the build instructions.
Making dependency file '/home/jeremy/projects/lean/library/standard/struc/wf.d' ...
error: file 'data/pair' not found in the LEAN_PATH
Making dependency file '/home/jeremy/projects/lean/library/standard/struc/binary.d' ...
On OSX, lean server crashes immediately when it opens a file. The following is an example input.
VISIT /Users/soonhok/work/lean/library/standard/logic/axioms/hilbert.lean
The following is the traces from valgrind:
$ valgrind ~/work/lean/bin/lean --server < input [22:27:42 on 14-08-15] ruby-1.9.3-p327
==31497== Memcheck, a memory error detector
==31497== Copyright (C) 2002-2013, and GNU GPL'd, by Julian Seward et al.
==31497== Using Valgrind-3.9.0 and LibVEX; rerun with -h for copyright info
==31497== Command: /Users/soonhok/work/lean/bin/lean --server
==31497==
==31497== WARNING: Support on MacOS 10.8/10.9 is experimental and mostly broken.
==31497== WARNING: Expect incorrect results, assertions and crashes.
==31497== WARNING: In particular, Memcheck on 32-bit programs will fail to
==31497== WARNING: detect any errors associated with heap-allocated data.
==31497==
--31497-- /Users/soonhok/work/lean/bin/lean:
--31497-- dSYM directory is missing; consider using --dsymutil=yes
!!!Interrupted!!!
==31497== Thread 2:
==31497== Invalid read of size 8
==31497== at 0x1000EC3E3: thread_specific_ptr<lean::memory_pool<48u> >::~thread_specific_ptr() (in /Users/soonhok/work/lean/bin/lean)
==31497== by 0xFD485: (anonymous namespace)::run(void*) (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libstdc++.6.dylib)
==31497== by 0x620478: _pthread_exit (in /usr/lib/system/libsystem_pthread.dylib)
==31497== by 0x61F8A3: _pthread_body (in /usr/lib/system/libsystem_pthread.dylib)
==31497== by 0x61F729: _pthread_start (in /usr/lib/system/libsystem_pthread.dylib)
==31497== by 0x623FC8: thread_start (in /usr/lib/system/libsystem_pthread.dylib)
==31497== Address 0x100f6c998 is 8 bytes inside a block of size 16 free'd
==31497== at 0x722F: free (in /usr/local/Cellar/valgrind/3.9.0/lib/valgrind/vgpreload_memcheck-amd64-darwin.so)
==31497== by 0x2CB802: emutls_destroy (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libgcc_s.1.dylib)
==31497== by 0x101: ???
==31497== by 0xB0080E9F: ???
==31497== by 0xB0080FFF: ???
==31497== by 0x62354E: _pthread_tsd_cleanup (in /usr/lib/system/libsystem_pthread.dylib)
==31497==
==31497== Invalid read of size 8
==31497== at 0x1000EC3EF: thread_specific_ptr<lean::memory_pool<48u> >::~thread_specific_ptr() (in /Users/soonhok/work/lean/bin/lean)
==31497== by 0xFD485: (anonymous namespace)::run(void*) (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libstdc++.6.dylib)
==31497== by 0x620478: _pthread_exit (in /usr/lib/system/libsystem_pthread.dylib)
==31497== by 0x61F8A3: _pthread_body (in /usr/lib/system/libsystem_pthread.dylib)
==31497== by 0x61F729: _pthread_start (in /usr/lib/system/libsystem_pthread.dylib)
==31497== by 0x623FC8: thread_start (in /usr/lib/system/libsystem_pthread.dylib)
==31497== Address 0x100f6c998 is 8 bytes inside a block of size 16 free'd
==31497== at 0x722F: free (in /usr/local/Cellar/valgrind/3.9.0/lib/valgrind/vgpreload_memcheck-amd64-darwin.so)
==31497== by 0x2CB802: emutls_destroy (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libgcc_s.1.dylib)
==31497== by 0x101: ???
==31497== by 0xB0080E9F: ???
==31497== by 0xB0080FFF: ???
==31497== by 0x62354E: _pthread_tsd_cleanup (in /usr/lib/system/libsystem_pthread.dylib)
==31497==
==31497== Invalid write of size 8
==31497== at 0x1000EC40B: thread_specific_ptr<lean::memory_pool<48u> >::~thread_specific_ptr() (in /Users/soonhok/work/lean/bin/lean)
==31497== by 0xFD485: (anonymous namespace)::run(void*) (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libstdc++.6.dylib)
==31497== by 0x620478: _pthread_exit (in /usr/lib/system/libsystem_pthread.dylib)
==31497== by 0x61F8A3: _pthread_body (in /usr/lib/system/libsystem_pthread.dylib)
==31497== by 0x61F729: _pthread_start (in /usr/lib/system/libsystem_pthread.dylib)
==31497== by 0x623FC8: thread_start (in /usr/lib/system/libsystem_pthread.dylib)
==31497== Address 0x100f6c998 is 8 bytes inside a block of size 16 free'd
==31497== at 0x722F: free (in /usr/local/Cellar/valgrind/3.9.0/lib/valgrind/vgpreload_memcheck-amd64-darwin.so)
==31497== by 0x2CB802: emutls_destroy (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libgcc_s.1.dylib)
==31497== by 0x101: ???
==31497== by 0xB0080E9F: ???
==31497== by 0xB0080FFF: ???
==31497== by 0x62354E: _pthread_tsd_cleanup (in /usr/lib/system/libsystem_pthread.dylib)
==31497==
==31497== Invalid read of size 8
==31497== at 0x10013265D: thread_specific_ptr<lean::memory_pool<32u> >::~thread_specific_ptr() (in /Users/soonhok/work/lean/bin/lean)
==31497== by 0xFD485: (anonymous namespace)::run(void*) (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libstdc++.6.dylib)
==31497== by 0x101: ???
==31497== by 0x102: ???
==31497== by 0xB0080E9F: ???
==31497== by 0x62354E: _pthread_tsd_cleanup (in /usr/lib/system/libsystem_pthread.dylib)
==31497== Address 0x100f63718 is 8 bytes inside a block of size 16 free'd
==31497== at 0x722F: free (in /usr/local/Cellar/valgrind/3.9.0/lib/valgrind/vgpreload_memcheck-amd64-darwin.so)
==31497== by 0x2CB802: emutls_destroy (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libgcc_s.1.dylib)
==31497== by 0x101: ???
==31497== by 0xB0080E9F: ???
==31497== by 0xB0080FFF: ???
==31497== by 0x62354E: _pthread_tsd_cleanup (in /usr/lib/system/libsystem_pthread.dylib)
==31497==
==31497== Invalid read of size 8
==31497== at 0x100132669: thread_specific_ptr<lean::memory_pool<32u> >::~thread_specific_ptr() (in /Users/soonhok/work/lean/bin/lean)
==31497== by 0xFD485: (anonymous namespace)::run(void*) (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libstdc++.6.dylib)
==31497== by 0x101: ???
==31497== by 0x102: ???
==31497== by 0xB0080E9F: ???
==31497== by 0x62354E: _pthread_tsd_cleanup (in /usr/lib/system/libsystem_pthread.dylib)
==31497== Address 0x100f63718 is 8 bytes inside a block of size 16 free'd
==31497== at 0x722F: free (in /usr/local/Cellar/valgrind/3.9.0/lib/valgrind/vgpreload_memcheck-amd64-darwin.so)
==31497== by 0x2CB802: emutls_destroy (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libgcc_s.1.dylib)
==31497== by 0x101: ???
==31497== by 0xB0080E9F: ???
==31497== by 0xB0080FFF: ???
==31497== by 0x62354E: _pthread_tsd_cleanup (in /usr/lib/system/libsystem_pthread.dylib)
==31497==
==31497== Invalid write of size 8
==31497== at 0x100132685: thread_specific_ptr<lean::memory_pool<32u> >::~thread_specific_ptr() (in /Users/soonhok/work/lean/bin/lean)
==31497== by 0xFD485: (anonymous namespace)::run(void*) (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libstdc++.6.dylib)
==31497== by 0x101: ???
==31497== by 0x102: ???
==31497== by 0xB0080E9F: ???
==31497== by 0x62354E: _pthread_tsd_cleanup (in /usr/lib/system/libsystem_pthread.dylib)
==31497== Address 0x100f63718 is 8 bytes inside a block of size 16 free'd
==31497== at 0x722F: free (in /usr/local/Cellar/valgrind/3.9.0/lib/valgrind/vgpreload_memcheck-amd64-darwin.so)
==31497== by 0x2CB802: emutls_destroy (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libgcc_s.1.dylib)
==31497== by 0x101: ???
==31497== by 0xB0080E9F: ???
==31497== by 0xB0080FFF: ???
==31497== by 0x62354E: _pthread_tsd_cleanup (in /usr/lib/system/libsystem_pthread.dylib)
==31497==
==31497== Invalid read of size 8
==31497== at 0x1001BB213: lean::list<lean::options>::~list() (in /Users/soonhok/work/lean/bin/lean)
==31497== by 0xFD485: (anonymous namespace)::run(void*) (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libstdc++.6.dylib)
==31497== by 0x101: ???
==31497== by 0x102: ???
==31497== by 0xB0080E9F: ???
==31497== by 0x62354E: _pthread_tsd_cleanup (in /usr/lib/system/libsystem_pthread.dylib)
==31497== Address 0x100f574c8 is 8 bytes inside a block of size 16 free'd
==31497== at 0x722F: free (in /usr/local/Cellar/valgrind/3.9.0/lib/valgrind/vgpreload_memcheck-amd64-darwin.so)
==31497== by 0x2CB802: emutls_destroy (in /usr/local/Cellar/gcc/4.9.1/lib/gcc/x86_64-apple-darwin13.2.0/4.9.1/libgcc_s.1.dylib)
==31497== by 0x101: ???
==31497== by 0xB0080E9F: ???
==31497== by 0xB0080FFF: ???
==31497== by 0x62354E: _pthread_tsd_cleanup (in /usr/lib/system/libsystem_pthread.dylib)
==31497==
==31497==
==31497== HEAP SUMMARY:
==31497== in use at exit: 154,708 bytes in 1,336 blocks
==31497== total heap usage: 5,207 allocs, 3,871 frees, 625,546 bytes allocated
==31497==
==31497== LEAK SUMMARY:
==31497== definitely lost: 0 bytes in 0 blocks
==31497== indirectly lost: 0 bytes in 0 blocks
==31497== possibly lost: 594 bytes in 30 blocks
==31497== still reachable: 128,364 bytes in 931 blocks
==31497== suppressed: 25,750 bytes in 375 blocks
==31497== Rerun with --leak-check=full to see details of leaked memory
==31497==
==31497== For counts of detected and suppressed errors, rerun with: -v
==31497== ERROR SUMMARY: 7 errors from 7 contexts (suppressed: 2003 from 107)
The idea is to force the library to be recompiled whenever we update the executable/version
lmake crashes if we execute it in any file at tests/lean/run. Here is the trace
Traceback (most recent call last):
File "../../../bin/lmake", line 187, in
sys.exit(main())
File "../../../bin/lmake", line 178, in main
directory = os.path.dirname(makefile)
File "/usr/lib/python2.7/posixpath.py", line 120, in dirname
i = p.rfind('/') + 1
AttributeError: 'bool' object has no attribute 'rfind'
FLYCHECK_BEGIN INFO
/home/soonhok/work/lean/library/standard/logic/axioms/hilbert.lean:23:68: type
Exists (λ (f : Π (3.1.14 : A), B 3.1.14), ∀ (x : A), P x (f x))
FLYCHECK_END
With
definition test {A B C : Type} (f : A → B) (x : C) := f x
I suggest the error message
type mismatch at application
f x
term
x
has type
C
but is expected to have type
A
This changes the current order of A and C, and also the wording slightly.
pre elaboration type information is not being deleted when elaboration succeeds
Currently goals are not pretty-printed, and extend beyond the end of the flycheck error window. (However, when the cursor is on the location, the goal is also displayed at information line at the bottom, which is longer.)
There are three issues here:
(1) goals should be displayed better
(2) the flycheck - lean interface should exchange information about line width
(3) some information (like goals) can appear in different contexts - in the error window, in the information line, and even in a popup - and different formatting is needed for each
It does not work on Linux.
I had to remove it to be able to compile the Lean libraries from scratch.
theorem test [coercion] ... : A -> B
is currently flagged as ambiguous, but the colon makes it unambiguous.
We can implement a pygments lexer for Lean and make a pull request as Agda and Idris people did:
Github will eventually pick a new version of pygments and use it.
open a file and enter the following:
import logic
theorem test (T : Type) (x : T) : x = x := refl _
theorem test2 (A : Type) (a : A) : a = a := test A a
Then make the first argument to test implicit:
theorem test {T : Type} (x : T) : x = x := refl _
Flycheck fails to report a error in test2 unless / until test2 is actually changed. With
#erase_cache test2
the behavior is corrected.
More emacs configuration could go in either the lean emacs mode or the flycheck mode. Two things that come to mind are:
(1) deleting trailing whitespace
(2) putting the error message window and compilation window to the right, by default
(3) setting the file window to 100 columns, by default
find gcd -- find theorems that use the constant gcd
find "gcd ?x ?y = gcd ?y ?x"
-- find theorems that match that pattern (anywhere)
find "gcd (gcd _ _) _" -- patterns with anonymous variables
find intro -- find any theorem whose conclusion unifies with your goal
find name: gcd -- find any theorem whose name contains "gcd"
These can be combined, e.g.
find intro gcd
find gcd name: assoc
find gcd "_ + 1"
define-derived-mode
and make it based on prog-mode
.idris-mode
define its syntax.Caro Leonardo,
Tentei compilar o Lean no meu Mac OS Mavericks, seguindo as instruções aqui: https://github.com/leodemoura/lean/blob/master/doc/make/cmake_make.md
cmake deu certo, mas make falhou. Segue abaixo a mensagem de erro:
release$ cmake -DCMAKE_BUILD_TYPE=RELEASE ../../src
-- Could NOT find TCMALLOC (missing: TCMALLOC_INCLUDE_DIR TCMALLOC_LIBRARIES)
*** WARNING: failed to find tcmalloc
*** The (optional) tcmalloc library is available at: https://code.google.com/p/gperftools
CMake Warning at CMakeLists.txt:125 (message):
FAILED to find tcmalloc, using standard malloc.
-- Usable malloc_usable_size was not detected
-- Found malloc_size
-- Found Lua: /usr/local/lib/liblua.dylib (found version "5.1.5")
-- lua_newstate works
-- Found PythonInterp: /Library/Frameworks/Python.framework/Versions/2.7/bin/python (found version "2.7.5")
-- Configuring done
-- Generating done
-- Build files have been written to: /Users/Bruno/Dropbox/Code/Lean/build/release
release$ make
Scanning dependencies of target util
[ 0%] Building CXX object util/CMakeFiles/util.dir/trace.cpp.o
[ 1%] Building CXX object util/CMakeFiles/util.dir/debug.cpp.o
[ 1%] Building CXX object util/CMakeFiles/util.dir/name.cpp.o
[ 1%] Building CXX object util/CMakeFiles/util.dir/name_set.cpp.o
[ 2%] Building CXX object util/CMakeFiles/util.dir/exception.cpp.o
/Users/Bruno/Dropbox/Code/Lean/src/util/exception.cpp:29:16: error:
thread-local storage is unsupported for the current target
static LEAN_THREAD_LOCAL std::string buffer;
^
/Users/Bruno/Dropbox/Code/Lean/src/util/thread.h:16:27: note: expanded from
macro 'LEAN_THREAD_LOCAL'
#define LEAN_THREAD_LOCAL thread_local
^
/Users/Bruno/Dropbox/Code/Lean/src/util/exception.cpp:41:12: error:
thread-local storage is unsupported for the current target
static LEAN_THREAD_LOCAL std::string buffer;
^
/Users/Bruno/Dropbox/Code/Lean/src/util/thread.h:16:27: note: expanded from
macro 'LEAN_THREAD_LOCAL'
#define LEAN_THREAD_LOCAL thread_local
^
2 errors generated.
make[2]: *** [util/CMakeFiles/util.dir/exception.cpp.o] Error 1
make[1]: *** [util/CMakeFiles/util.dir/all] Error 2
make: *** [all] Error 2
Can we change the output convention for type information?
--typeinfo
--typeinfo
takes an optional argument --typeinfo <LINE_NO>
: If LINE_NO
is specified, lean only reports type information at the specified line LINE_NO
, otherwise it reports all type information in a file.|
as a delimiter. Note that <TYPE_OF_ID> doesn't have a newline \n
in itTYPE|<FILENAME>|<LINE_NO>|<COL>|<TYPE_OF_ID>
Example:
TYPE|/home/soonhok/work/lean/library/standard/logic/connectives/basic.lean|154|69|(a → b) → (b → a) → and (a → b) (b → a)
TYPE|/home/soonhok/work/lean/library/standard/logic/connectives/basic.lean|154|79|a → b
TYPE|/home/soonhok/work/lean/library/standard/logic/connectives/basic.lean|154|82|b → a
With
inductive ... : Type :=
...
we could allow the user to omit ": Type".
tactics such as (apply t) and (exact t) must elaborate t modulo the current goal.
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.
Use the latest snapshot of gcc-4.8 in MXE.
Let's consider
section foo
...
end foo
and
namespace foo
...
end foo
Should we require that all sections and namespaces be closed at the end of a file?
ltags
takes *.ilean
files and generates TAGS
file, possibliy supporting multiple tag systems such as etags
and global
.
Recently, we had a problem in pushing to bitbucket in travis-ci, and disabled the feature. One side effect of it is that we don't get commit email notification with full diff of changes. For now, I enabled github's email notification feature. Unfortunately, github does not support email diff and has no plan to do it. I'll see how to fix the original bitbucket problem.
The tactic language needs these (like Coq's).
I was testing the lean-show-type function, and found a problem with INSERT
command.
First, open library/standard/data/list/basic.lean
file and send a query about line 280:
VISIT /home/soonhok/work/lean/library/standard/data/list/basic.lean
INFO 280
/home/soonhok/work/lean/library/standard/data/list/basic.lean:17:0: warning: imported file uses 'sorry'
-- BEGININFO
-- TYPE|280|21
Type
-- ACK
-- TYPE|280|29
Type → Type
-- ACK
-- TYPE|280|34
Type
-- ACK
-- TYPE|280|42
Type
-- ACK
-- TYPE|280|47
Type
-- ACK
-- ENDINFO
Good, let's insert "-- comment" at line 280.
INSERT 280
-- comment
I expect we have the same information at line 281 (since the old line 280 is shifted to 281)
INFO 281
/home/soonhok/work/lean/library/standard/data/list/basic.lean:225:0: warning: imported file uses 'sorry'
-- BEGININFO
-- ENDINFO
There is nothing. To make sure, I send more queries:
INFO 280
-- BEGININFO
-- ENDINFO
INFO 279
-- BEGININFO
-- ENDINFO
INFO 282
-- BEGININFO
-- ENDINFO
INFO 283
-- BEGININFO
-- ENDINFO
Note that I added -- BEGININFO
at the beginning of INFO messages.
E.g. make produced the following "congr.d":
/home/jeremy/projects/lean/library/standard/logic/classes/congr.olean : /home/jeremy/projects/lean/library/standard/logic/classes/cong
r.lean /home/jeremy/projects/lean/library/standard/logic/classes/congr.d error: file 'logic/connectives/function' not found in the LEA
N_PATH
Then make produced the following error message:
/home/jeremy/projects/lean/library/standard/logic/classes/congr.d:1: *** multiple target patterns. Stop.
Instead, the first failure should raise the error and not produce the .d file.
Parser for SMT 2.0
It should be a configuration option.
The default can be something like 0.4 secs.
Implement the following behavior for namespaces:
namespace foo
theorem bar : ...
end foo
creates identifier foo.bar.
"import" and "namespace" are kept orthogonal (file structure has nothing to do with namespace structure).
The command
open foo [as bar] [using / hiding / renaming]
does the following (conceptually):
(1) gathers all the theorems in foo, removing "foo"
(2) picks out the ones indicated by using / hiding
(3) renames according to renaming
(4) creates aliases, prepending "bar" if present
The command
export foo [as bar] [using / hiding / renaming]
does the same thing but creates permanent abbreviations rather than transient aliases.
Question: should we have special syntax for opening / exporting a single theorem? E.g.
open foo bar
or
open foo (bar)
for
open foo (using bar)
Inside a module, a theorem or definition can be marked as "private", which means that it is never opened or exported. It can also be marked as "protected", which means that it is never opened or exported unless the user explicitly asks for it.
Question: what should the syntax for that be? We can require that it is on an explicit "using" list. In that case, the user would have to say
open nat
open nat (using induction_on)
possibly with the shorthand above. Another option is to add another modifier, "including", which can be used in the absence of using. So
open nat (including induction_on)
would have the same meaning as the two lines above.
Add options to flag an error or warning if identifies become overloaded, and also if notation conflicts.
A command
theorem foo [in bar] ...
puts the theorem in bar (i.e. calls it bar.foo) but also uses it, i.e. creates an alias.
The command
inductive foo : Type :=
| bar : ...
| baz : ...
creates constants foo, foo.mk, foo.rec, foo.bar, foo.baz, and similarly for "structure".
The construct
section
end
should be used to set parameters common to all theorems. Notations, rewrites, and so on are persistent.
The construct
context
end
should be used to set up a local context. Notations, rewrites, and so on are transient.
We need to re-implement it and cleanup.
We also need a higher-order unification procedure that is independent of the elaborator because it does too much. For example, we don't want to unfold definitions or apply beta-reduction.
if foo defines a coercion, then every time foo is imported, the "coercion is replaced", e.g.
replacing the coercion from 'num.num' to 'nat.nat'
replacing the coercion from 'num.num' to 'nat.nat'
when the nat library is imported (with files basic, order, sub).
Suppose we have
namespace foo
namespace bar
theorem baz
...
end
end
If we import this from another file, we can refer to
foo.bar.baz
If we then say
using foo
it would be convenient if we then could refer to the theorem as
bar.baz
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.