unimath / schools Goto Github PK

TeX 30.56% Coq 46.97% Emacs Lisp 0.12% Makefile 0.20% HTML 21.59% CSS 0.56%

schools's Introduction

Univalent Mathematics

This Coq library aims to formalize a substantial body of mathematics using the univalent point of view.

Trying out UniMath

You can try out UniMath in the browser by clicking here. For instance, you can run the files from the School on Univalent Mathematics in the browser.

Using UniMath on your computer

To install UniMath on your computer, there are two options:

Install a released binary version of UniMath via the Coq Platform.
To develop, and contribute to, UniMath, you should compile the latest version of UniMath yourself - see INSTALL.md.

Usage

See USAGE.md

The UniMath subdirectory contains various packages of formalized mathematics. For more information, see the UniMath Table of Contents.

Some scientific articles describing the contents of the UniMath library or work using it are listed in the wiki.

Contributing to UniMath

To contribute to UniMath, submit a pull request. Your code will be subject to the copyright and license agreement in LICENSE.md.

For the style guide and other instructions, see UniMath/README.md.

Discussing UniMath & Getting Help

Questions about the UniMath library, compilation, and installation of UniMath, etc., can be asked in the UniMath Zulip (click here to register) or on the UniMath mailing list (archived in a Google Group).
Bugs should be reported in our UniMath bug tracker on GitHub.

Citing UniMath

To cite UniMath in your article, you can use the following bibtex item:

@Misc{UniMath,
    author = {Voevodsky, Vladimir and Ahrens, Benedikt and Grayson, Daniel and others},
    title = {UniMath --- a computer-checked library of univalent mathematics},
    url = {https://github.com/UniMath/UniMath},
    howpublished = {available at \url{http://unimath.org}},
    doi          = {10.5281/zenodo.10849216},
    url          = {https://doi.org/10.5281/zenodo.10849216}
 }

Note that this requires \usepackage{url} or \usepackage{hyperref}.

The UniMath Coordinating Committee

The UniMath project was started in 2014 by merging the repository Foundations, by Vladimir Voevodsky (written in 2010), with two repositories based on it: rezk_completion, by Benedikt Ahrens, and Ktheory, by Daniel Grayson. Vladimir Voevodsky was a member of the team until his death in September, 2017.

The current members of the UniMath Coordinating Committee are:

Benedikt Ahrens
Daniel Grayson
Michael Lindgren
Peter LeFanu Lumsdaine
Ralph Matthes
Niels van der Weide

Acknowledgments

The UniMath development team gratefully acknowledges the great work by the Coq development team in providing the Coq proof assistant, as well as their support in keeping UniMath compatible with Coq.

schools's People

Contributors

Stargazers

Watchers

Forkers

dangrayson bts8394 tomdjong mortberg andrejbauer ekim1919 paulcadman faineance annamiraotoole erikmd elisabethstenholm sprinterzzj benediktahrens paigenorth piggiosauro nabil-atlam skantz drruisseau novusnota-forks

schools's Issues

Compilation fails

@DanGrayson : can you help with this? It happens on a fresh clone of current Workshops.

/tmp/Workshops$ make
make -C UniMath TAGS all
make[1]: Entering directory '/tmp/Workshops/UniMath'
make[1]: *** No rule to make target 'TAGS'.  Stop.
make[1]: Leaving directory '/tmp/Workshops/UniMath'
Makefile:4: recipe for target 'build_UniMath' failed
make: *** [build_UniMath] Error 2

Compile less of UniMath

Do not compile (by default) packages that are not needed for the School (and take long to compile):

SubstitutionSystems
HomologicalAlgebra
Ktheory

Cannot step through Workshop files in Emacs

When stepping through 2017-12-Birmingham/Part2_Fundamentals_Coq/coq_exercises.v:

Error:
The file /home/ahrens/git/UniMath/Workshops/2017-12-Birmingham/Part2_Fundamentals_Coq/fundamentals_lecture.vo contains library
Bham2017.fundamentals_lecture and not library fundamentals_lecture

@DanGrayson : can you help with this?

I imagine it would be best to have fully qualified import statements in the workshop files, just like we have in UniMath.

Provide solutions for CT exercises

Part5 : assert by to be replaced by something else?

course material for several parts is missing in this repository

Links to places where the material can be found would be helpful - if the files are not placed here.

lecture 2: replace \^ by ^

Part1: translate pdf into markdown

and mark difficult exercises with a (*)

Error when running make file; probably Schools points to old version of Coq?

Last bit of terminal output:

clang: warning: optimization flag '-fexcess-precision=standard' is not supported [-Wignored-optimization-argument]
OCAMLC kernel/byterun/coq_memory.c
clang: warning: optimization flag '-fexcess-precision=standard' is not supported [-Wignored-optimization-argument]
OCAMLC kernel/byterun/coq_values.c
clang: warning: optimization flag '-fexcess-precision=standard' is not supported [-Wignored-optimization-argument]
OCAMLC kernel/byterun/coq_interp.c
clang: warning: optimization flag '-fexcess-precision=standard' is not supported [-Wignored-optimization-argument]
cd kernel/byterun/ &&
"/usr/local/bin/ocamlfind" ocamlmklib -oc coqrun coq_fix_code.o coq_memory.o coq_values.o coq_interp.o
COQMKTOP -o bin/coqtop.opt
Undefined symbols for architecture x86_64:
"_caml_young_limit", referenced from:
_coq_interprete in libcoqrun.a(coq_interp.o)
"_caml_young_ptr", referenced from:
_coq_interprete in libcoqrun.a(coq_interp.o)
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
File "caml_startup", line 1:
Error: Error during linking (exit code 1)
make[3]: *** [bin/coqtop.opt] Error 2
make[3]: Leaving directory /Users/joegould/Documents/Schools/UniMath/sub/coq' make[2]: *** [submake] Error 2 make[2]: Leaving directory /Users/joegould/Documents/Schools/UniMath/sub/coq'
make[1]: *** [sub/coq/bin/coq_makefile] Error 2
make: *** [build_UniMath] Error 2

Error: Cannot find a physical path bound to logical path matching suffix UniMath.MoreFoundations.

Indeed, I cannot import any UniMath file in this Coq file. This is strange, since the import works in other files, in Part1 and Part2.

@DanGrayson : can you help? I am entirely clueless about this.

Set up Travis

see #9