From 3a20b6be8a570eb2027675aee1ca2206c7b73b8a Mon Sep 17 00:00:00 2001 From: Chris Lovett Date: Thu, 23 Sep 2021 00:21:39 -0700 Subject: [PATCH] doc: add wsl setup docs and reorganize a new "dev" folder --- doc/SUMMARY.md | 14 +- doc/coding_style.md | 244 ----------------------------- doc/dev/bootstrap.md | 122 +++++++++++++++ doc/{ => dev}/commit_convention.md | 0 doc/dev/cpp_coding_style.md | 155 ++++++++++++++++++ doc/{ => dev}/debugging.md | 0 doc/{ => dev}/fixing_tests.md | 0 doc/dev/index.md | 71 +++++++++ doc/{ => dev}/mdbook.md | 0 doc/dev/testing.md | 98 ++++++++++++ doc/images/code-wsl.png | Bin 0 -> 38683 bytes doc/make/emscripten.md | 3 +- doc/make/index.md | 185 +--------------------- doc/make/msvc.md | 17 +- doc/make/msys2.md | 17 +- doc/make/nix.md | 14 +- doc/make/osx-10.9.md | 42 ++--- doc/make/ubuntu-16.04.md | 12 +- doc/make/wsl.md | 56 +++++++ doc/make/wsl2.md | 1 + 20 files changed, 572 insertions(+), 479 deletions(-) delete mode 100644 doc/coding_style.md create mode 100644 doc/dev/bootstrap.md rename doc/{ => dev}/commit_convention.md (100%) create mode 100644 doc/dev/cpp_coding_style.md rename doc/{ => dev}/debugging.md (100%) rename doc/{ => dev}/fixing_tests.md (100%) create mode 100644 doc/dev/index.md rename doc/{ => dev}/mdbook.md (100%) create mode 100644 doc/dev/testing.md create mode 100644 doc/images/code-wsl.png create mode 100644 doc/make/wsl.md create mode 100644 doc/make/wsl2.md diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md index 9c6b306b92..f2bc424987 100644 --- a/doc/SUMMARY.md +++ b/doc/SUMMARY.md @@ -55,12 +55,16 @@ # Development -- [Commit Convention](./commit_convention.md) +- [Development Guide](./dev/index.md) +- [Commit Convention](./dev/commit_convention.md) - [Building Lean](./make/index.md) - [Ubuntu Setup](./make/ubuntu-16.04.md) - [macOS Setup](./make/osx-10.9.md) - - [Windows Setup](./make/msys2.md) + - [Windows MSYS2 Setup](./make/msys2.md) + - [Windows with WSL](./make/wsl2.md) - [Nix Setup (*Experimental*)](./make/nix.md) -- [Building This Manual](./mdbook.md) -- [Fixing Tests](./fixing_tests.md) -- [Debugging](./debugging.md) +- [Unit Testing](./dev/testing.md) +- [Building This Manual](./dev/mdbook.md) +- [Fixing Tests](./dev/fixing_tests.md) +- [Debugging](./dev/debugging.md) +- [C++ Coding Style](./dev/cpp_coding_style.md) \ No newline at end of file diff --git a/doc/coding_style.md b/doc/coding_style.md deleted file mode 100644 index 774afebd10..0000000000 --- a/doc/coding_style.md +++ /dev/null @@ -1,244 +0,0 @@ -Coding Style -============ - -[C++11](http://en.wikipedia.org/wiki/C%2B%2B11) features --------------------------------------------------------- - -We make extensive use of new features in the C++ 11 standard. -Developers must be familiar with the standard to be able to understand -the code. -Here are some of the features that are extensively used. - -- Type inference (aka `auto` keyword). -- Initializer lists. -- Lambda functions and expressions. -- `nullptr` constant. -- Strongly typed enumerations. -- Right angle bracket. -- Thread local storage. -- Threading facilities. -- Tuple types. - -Comments --------- - -The comments in the Lean codebase contain -[Doxygen](http://www.stack.nl/~dimitri/doxygen/) commands. -Doxygen is the de facto standard tool for generating documentation from -annotated C++ sources. - -Namespaces ----------- - -All code is in the `lean` namespace. Each frontend is stored in a -separate nested namespace. For example, the SMT 2.0 frontend is stored -in the `lean::smt` namespace. - -Exception: some debugging functions are stored outside of the `lean` -namespace. These functions are called `print` and are meant to be used -when debugging Lean using `gdb`. - -Smart pointers --------------- - -We only use `std::shared_ptr` template for class `C` only if we expect -to create only a few objects (< 1000) of class `C`. Otherwise, we -implement our own intrusive smart pointer. For example, the class -`expr` is an intrusive smart pointer to `expr_cell`. We may have -millions of `expr` objects. We say it is intrusive because the -reference counter is stored in `expr_cell`. - -We use `std::unique_ptr` to make sure unique resources will be freed -correctly. - -Template --------- -We organize template source code using the approach described at http://www.codeproject.com/Articles/3515/How-To-Organize-Template-Source-Code - -Idioms ------- - -We use some popular C++ idioms: - -- [Pimpl](http://c2.com/cgi/wiki?PimplIdiom) -- [RAII](http://en.wikipedia.org/wiki/Resource_Acquisition_Is_Initialization) Resource Acquisition Is Initialization - -Formatting ----------- - -* We use 4 spaces for indentation. - -* Class, method, and function names are lower case -We use `_` for composite names. Example: `type_checker`. - -* Class/struct fields should start with the prefix `m_`. - -Example: - - class point { - int m_x; - int m_y; - public: - ... - }; - -* We do **not** use the `#ifndef-#define-#endif` idiom for header files. -Instead we use `#pragma once`. - -* We write `type const & v` instead of `const type & v`. - -* We use `const` extensively. - -* `if-then-else` - -The following forms are acceptable: - - if (cond) { - ... - } else { - ... - } - -and - - if (cond) - statement1; - else - statement2; - -In *exceptional cases*, we also use - - if (cond) statement; - -and - - if (cond) statement1; else stament2; - -* `if-then-else-if-else` - -The following forms are acceptable: - - if (cond) { - ... - } else if (cond) { - ... - } else { - ... - } - -and - - if (cond) - statement1; - else if (cond) - statement2; - else - statement3; - -* We frequently format code using extra spaces - -For example, we write - - environment const & m_env; - cache m_cache; - normalizer m_normalizer; - volatile bool m_interrupted; - -instead of - - environment const & m_env; - cache m_cache; - normalizer m_normalizer; - volatile bool m_interrupted; - -* We use the macro `lean_assert` for assertions. -The macro `lean_assert` is extensively used when writing unit tests. - -* Spaces in expressions -We write `a == b` instead of `a==b`. -Similarly, we write `x < y + 1` instead of `x``. If you need to cast within a class - hierarchy, use ``static_cast<>`` to upcast. Google doesn't support - RTTI. - - "public:" should be preceded by a blank line - - Missing space before ``{`` - - Found C system header after C++ system header. Should be: - environment.h, c system, c++ system, other. - - Labels should always be indented at least one space. If this is - a member-initializer list in a constructor or the base class list in - a class definition, the colon should be on the following line. - - You don't need a ``;`` after a ``}`` - - No ``#ifndef`` header guard found - - Streams are highly discouraged. - - Extra space before ``(`` in function call - - Else clause should never be on same line as else - - Extra space before ``)`` - - Is this a non-const reference? If so, make const or use a pointer. - - All parameters should be named in a function - - Do not use anonymous constructor notation (e.g., ``{a1, ..., an}``) - -Modified Features: - - - Add ``#include `` for ``list<>`` - - => *Check* ``std::list`` instead of ``list`` because we do have our own ``lean::list`` type. - - - Add ``#include `` for copy - - => *Check* ``std::copy`` instead of ``copy`` because we do have our own ``lean::copy`` method. - - - Do not use namespace using-directives. Use using-declarations instead. - - => *Allow* this if filename contains "tests/" - - - Small and focused functions are preferred: foo() - has xxx non-comment lines (error triggered by exceeding 500 lines). - - => *Allow* this if filename contains "tests/" - - - Include the directory when naming .h files - - => *Allow* this if the included filename is "version.h" which is generated by cmake. - -[google-style]: http://google-styleguide.googlecode.com/svn/trunk/cppguide.xml -[cpplint]: /src/cmake/Modules/cpplint.py - -Git pre-push hook ------------------ - -Since [git 1.8.2][git-pre-push-hook], git introduced *pre-push* hook -which is executed *before* actual push operation is performed. Using this, -we can *automatically* run the style checker over the changed files *before* -we push commits to repositories. This is useful because it prevents us -from accidentally pushing the commits which contain style problems. - -[git-pre-push-hook]: https://github.com/git/git/blob/master/Documentation/RelNotes/1.8.2.txt - -To activate the hook, execute - -```bash -ln -s ../../script/pre-push .git/hooks -``` - -in the project root directory. - -You can change the ``CHECKER`` variable in the script if you want to use other -checkers. diff --git a/doc/dev/bootstrap.md b/doc/dev/bootstrap.md new file mode 100644 index 0000000000..f4fcb24bc3 --- /dev/null +++ b/doc/dev/bootstrap.md @@ -0,0 +1,122 @@ + +# Lean Build Bootstrapping + +Since version 4, Lean is a partially bootstrapped program: most parts of the +frontend and compiler are written in Lean itself and thus need to be built before +building Lean itself - which is needed to again build those parts. This cycle is +broken by using pre-built C files checked into the repository (which ultimately +go back to a point where the Lean compiler was not written in Lean) in place of +these Lean inputs and then compiling everything in multiple stages up to a fixed +point. The build directory is organized in these stages: + +```bash +stage0/ + # Bootstrap binary built from stage0/src/. + # We do not use any other files from this directory in further stages. + bin/lean +stage1/ + include/ + config.h # config variables used to build `lean` such as use allocator + runtime/lean.h # runtime headers, used by extracted C code, uses `config.h` + share/lean/ + Makefile # used by `leanmake` + lib/ + lean/**/*.olean # the Lean library (incl. the compiler) compiled by the previous stage's `lean` + temp/**/*.{c,o} # the library extracted to C and compiled by `leanc` + libInit.a libStd.a libLean.a # static libraries of the Lean library + libleancpp.a # a static library of the C++ sources of Lean + bin/ + lean # the Lean compiler & server linked together from the above libraries + leanc # a wrapper around a C compiler supplying search paths etc + leanmake # a wrapper around `make` supplying the Makefile above +stage2/... +stage3/... +``` + +Stage 0 can be viewed as a blackbox since it does not depend on any local +changes and is equivalent to downloading a bootstrapping binary as done in other +compilers. The build for any other stage starts by building the runtime and +standard library from `src/`, using the `lean` binary from the previous stage in +the latter case, which are then assembled into a new `bin/lean` binary. + +Each stage can be built by calling `make stageN` in the root build folder. +Running just `make` will default to stage 1, which is usually sufficient for +testing changes on the test suite or other files outside of the stdlib. However, +it might happen that the stage 1 compiler is not able to load its own stdlib, +e.g. when changing the .olean format: the stage 1 stdlib will use the format +generated by the stage 0 compiler, but the stage 1 compiler will expect the new +format. In this case, we should continue with building and testing stage 2 +instead, which will both build and expect the new format. Note that this is only +possible because when building a stage's stdlib, we use the previous compiler +but never load the previous stdlib (since everything is `prelude`). We can also +use stage 2 to test changes in the compiler or other "meta" parts, i.e. changes +that affect the produced (.olean or .c) code, on the stdlib and compiler itself. +We are not aware of any "meta-meta" parts that influence more than two stages of +compilation, so stage 3 should always be identical to stage 2 and only exists as +a sanity check. + +In summary, doing a standard build via `make` involves these steps: + +1. compile the `stage0/src` archived sources into `stage0/bin/lean` +1. use it to compile the current library (*including* your changes) into `stage1/lib` +1. link that and the current C++ code from `src/` into `stage1/bin/lean` + +You now have a Lean binary and library that include your changes, though their +own compilation was not influenced by them, that you can use to test your +changes on test programs whose compilation *will* be influenced by the changes. + +Finally, when we want to use new language features in the library, we need to +update the stage 0 compiler, which can be done via `make -C stageN update-stage0`. +`make update-stage0` without `-C` defaults to stage1. + +## Further Bootstrapping Complications + +As written above, changes in meta code in the current stage usually will only +affect later stages. This is an issue in two specific cases. + +* For *non-builtin* meta code such as `notation`s or `macro`s in + `Notation.lean`, we expect changes to affect the current file and all later + files of the same stage immediately, just like outside the stdlib. To ensure + this, we need to build the stage using `-Dinterpreter.prefer_native=false` - + otherwise, when executing a macro, the interpreter would notice that there is + already a native symbol available for this function and run it instead of the + new IR, but the symbol is from the previous stage! + + To make matters more complicated, while `false` is a reasonable default + incurring only minor overhead (`ParserDescr`s and simple macros are cheap to + interpret), there are situations where we *need* to set the option to `true`: + when the interpreter is executed from the native code of the previous stage, + the type of the value it computes must be identical to/ABI-compatible with the + type in the previous stage. For example, if we add a new parameter to `Macro` + or reorder constructors in `ParserDescr`, building the stage with the + interpreter will likely fail. Thus we need to set `interpreter.prefer_native` + to `true` in such cases to "freeze" meta code at their versions in the + previous stage; no new meta code should be introduced in this stage. Any + further stages (e.g. after an `update-stage0`) will then need to be compiled + with the flag set to `false` again since they will expect the new signature. + + For an example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb. + +* For the special case of *quotations*, it is desirable to have changes in + built-in parsers affect them immediately: when the changes in the parser + become active in the next stage, macros implemented via quotations should + generate syntax trees compatible with the new parser, and quotation patterns + in macro and elaborators should be able to match syntax created by the new + parser and macros. Since quotations capture the syntax tree structure during + execution of the current stage and turn it into code for the next stage, we + need to run the current stage's built-in parsers in quotation via the + interpreter for this to work. Caveats: + * Since interpreting full parsers is not nearly as cheap and we rarely change + built-in syntax, this needs to be opted in using `-Dinternal.parseQuotWithCurrentStage=true`. + * The parser needs to be reachable via an `import` statement, otherwise the + version of the previous stage will silently be used. + * Only the parser code (`Parser.fn`) is affected; all metadata such as leading + tokens is taken from the previous stage. + + For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422 + (from before the flag defaulted to `false`). + +To modify either of these flags both for building and editing the stdlib, adjust +the code in `stage0/src/stdlib_flags.h`. The flags will automatically be reset +on the next `update-stage0` when the file is overwritten with the original +version in `src/`. \ No newline at end of file diff --git a/doc/commit_convention.md b/doc/dev/commit_convention.md similarity index 100% rename from doc/commit_convention.md rename to doc/dev/commit_convention.md diff --git a/doc/dev/cpp_coding_style.md b/doc/dev/cpp_coding_style.md new file mode 100644 index 0000000000..6cf2aceb40 --- /dev/null +++ b/doc/dev/cpp_coding_style.md @@ -0,0 +1,155 @@ +[google-style]: https://google.github.io/styleguide/cppguide.html +[cpplint]: /src/cmake/Modules/cpplint.py + +# Coding Style + +The Lean project is moving away from using any C++ as more and more of +the compiler is being bootstrapped in Lean itself. But the remaining +C++ codebase is using modified version of [Google's C++ Style +Guide][google-style]. + +## [C++11](http://en.wikipedia.org/wiki/C%2B%2B11) features + +Lean makes extensive use of new features in the C++ 11 standard. +Developers must be familiar with the standard to be able to understand +the code. Here are some of the features that are extensively used. + +- Type inference (aka `auto` keyword). +- Initializer lists. +- Lambda functions and expressions. +- `nullptr` constant. +- Strongly typed enumerations. +- Right angle brackets with no space is now allowed in C++ 11. +- Thread local storage. +- Threading facilities. +- Tuple types. +- Smart pointers. +- When using ``std::list`` make sure to include the `std::` + qualifier so you do not accidentally use the ``lean::list`` type. +- When using ``std::copy`` make sure to include the `std::` + qualifier so you do not accidentally use the ``lean::copy`` type. +- Small and focused functions are preferred: foo(). Try not to + exceed 500 lines in a function, except in tests. +- Do **not** use the `#ifndef-#define-#endif` idiom for header files. + Instead use `#pragma once`. +- Write `type const & v` instead of `const type & v`. +- Use `const` extensively. +- Use the macro `lean_assert` for assertions. The macro `lean_assert` + is extensively used when writing unit tests. + +## Naming + +- Class, method, and function names are lower case +Use `_` for composite names. Example: `type_checker`. +- Class/struct fields should start with the prefix `m_`. + + Example: + ```c++ + class point { + int m_x; + int m_y; + public: + ... + }; + ``` + +## Namespaces + +All code is in the `lean` namespace. Each frontend is stored in a +separate nested namespace. For example, the SMT 2.0 frontend is stored +in the `lean::smt` namespace. + +Exception: some debugging functions are stored outside of the `lean` +namespace. These functions are called `print` and are meant to be used +when debugging Lean using `gdb`. + +Do not use `using namespace` in a header file. + +## Templates + +Organize template source code using the approach described at http://www.codeproject.com/Articles/3515/How-To-Organize-Template-Source-Code + +## Idioms + +Use some popular C++ idioms: + +- [Pimpl](http://c2.com/cgi/wiki?PimplIdiom) +- [RAII](http://en.wikipedia.org/wiki/Resource_Acquisition_Is_Initialization) Resource Acquisition Is Initialization + +## Formatting + +* Use 4 spaces for indentation. + +* `if-then-else` curly brackets not always required. The following + forms are acceptable: + + ```c++ + if (cond) { + ... + } else { + ... + } + ``` + and + + ```c++ + if (cond) + statement1; + else + statement2; + ``` + + In *exceptional cases*, we also use + + ```c++ + if (cond) statement; + ``` + + and + + ```c++ + if (cond) statement1; else stament2; + ``` + * `if-then-else-if-else` + + The following forms are acceptable: + + ```c++ + if (cond) { + ... + } else if (cond) { + ... + } else { + ... + } + ```c++ + and + + ```c++ + if (cond) + statement1; + else if (cond) + statement2; + else + statement3; + ``` + +* Format code using extra spaces to make code more readable. For example: + + ```c++ + environment const & m_env; + cache m_cache; + normalizer m_normalizer; + volatile bool m_interrupted; + ``` + instead of: + + ```c++ + environment const & m_env; + cache m_cache; + normalizer m_normalizer; + volatile bool m_interrupted; + ``` + +* Spaces in expressions. Write `a == b` instead of `a==b`. Similarly, + we write `x < y + 1` instead of `xkFo5}HJ$Lqe|#B2uJ>UZhJ45_&=r zkd{!C-a`w$NN9%o1s|XDp7%TFyT0r9`vY?Ao$R&N%$hZG&poq)pJ^&zre>k0prE*{ z@>EfWg5q2a1;ts^g|p;4=`P_@)#8d9QRlUYw~QF$_;LF3+*huRehrkksGx97kd0OTJ$&mpuSsG}k2cM(-jlR1UTb@OQgMEYp27Q%Ccb zXSXTRf1?GKcw21+;{~aDcDs5cTIp?`+DFs|Ngj6Pnmr2H^-JrP^J>bbEo? zR2HB<&3_dzlt;fbJ4#TcGps+-p*PV2!rc~~1F~MrZApgF0(-b!e*6qh6iIJaiUU|4 zACj1iy+`Ic{ae)Pt_jD1B^P+*pI)k2l!@<2@%gc2nSPMxAhpBqC)}*0XYeaaZa)j& z4P5Z25vcw(6N=wT+XJ5`?*PRWs`#YNn(}$r=Db@faE0HGxSIlKIEmFgUW=_dE~)CC z6gA>AC_H!i+iy?1pm3zb-l5v@So(Y`;$$)6__gcMs#*zs`tQL$u*`lF1=X%}COVK} zs*-_N5zFpccOfq9>C+VN)gBa*XTr+)jOFJYZgQM#QZj)*wfz3>78(pEkr(ZS4PzD& zKreFg|DN&9T$Zm$4`wm8tXtBiAMfe3R54^SN}9w~;z?H|(&$p!NQ7fM zwYvIus6BcPZwh$eug9;RboTZfCeNWJo0)oya>stplqGJ7cII|fD;oFM9`3K?8x&pwFR&!`SzBs*DTRJD#XIVOIliw746V^rCR ztVca3Bsqub>GP1Fn2*lfOLe`8E;4U~cE5&1*7N#20Z~wxhP=c(ha(<|sZbV6cGqtB zY#g+T*E=1oRe5Rh73$ni&h}@d6hQ&f8?tvMIF83g3M(-i#`Ui~+AvfNQ^IAw2QCqZ z$)WlMe>w39@z-Uxg?kL@K|qXN-<$8yg|D+mBYB0nW(JAx3oaBjTC|k4}9rf^@=7#<@lD~+L@*w+Ag(e z2le}%K1R;a+RsfM)K#pa7~BX}zTj$~yRQq*r-xO_GnCK!R=(X+eY=heZDOM3sKvXa+$|HNCrc)WW+CrFc&zmWLA}CBZE0TNyi!63^fx;LsLjCXEH^-N zY>Jb(-uF}Y%dDioXdZSs_=*(c5(B5bx9h2t9SLPs6JD*w`1o3{*;FPIr><3Ks^ukV z-`2^Vu}!_sIL>SdRLNaIrECewb6$PUy@UVXpGh|dF~~)(op9-nZd0Gu?Lr) z6ixlK)?ZozxI%fH=t$@G?gV{ad@&tyKZsRmM;dKu_m?9fKeRSL{Thf-T4YzhLg#Ln zH1aSl3213ox6p4?Z%LeVNENS6ZO5ZDQ_kS*VBK!GpdYlf(SfjT)kI?u>-Rw)p@pnZbfdxZ&wH8;s_s>7M|*- zYT;U{0$n}m^UOFtVD7Q6fA`0*AfjbUxBIvQHIKn;2VW_H=KCEil&BKvhh9#9S&hhE z@w)YxF`O01$@DC3KiM9w!iy`ALKbgy-}cF{P$n(BTN7O0$C((2QME6>MR4*DKVgME zbE~n4k$JXXI=oK=#ZekHu3h6UMWbkQSvpA^GRyiEnz@XYjEqw}vlh;TCS`4Y-EDUF zMh4fgLO?_%hyDun*Kb@Kw}=8S@g~w(TNb$#4t&%tnk+`>?br20FM&cJd`tP2_mo$X zjETfcXbJuDt7+Ymd0k+l{8C*qR(`(@JgH0QH9A*#!4gQj@@ZGYkoNXjGeG;>B1|?Q z>@3ia`#$a7C-Ch0j~u#%)PTBMD9Jvxo^sJeIPi;l&EgBPnPDe(R~2%E=L z_fLzO{+htZ`pQYCH4y;KlBNE-w~>8MBmWp%pVqt8MOMQ&N`pv+;l4PSmHu(ATRuGy zDRU->wWacbp9n`NB(h=sELtRrAklFx@bE-ZOG;1QOny}Rn**O=bSa2akC^w#QL(@= zOIsNHA{^19}UkR`Oqrrx!bTJ6>bOwS=_?8br$FhpZPQc~BB5QUh}1 z07AHar!D?$Exm}ihY23hBuRsamgs(!)R^t-6D|FnwqigIBSPWc1Xs>02RHNlV#>=# zIs?=^()P5#+_;JOf%?4{rZ7(OCh0ifGfp=NR3zXBFyqVQ3zMc&sNO~;^?}xWSLz>} z?8%+18{tnH<~FQSgC=!jn7^IlK3bS_y{j$RZn8L5l0e~AsQW_wdw!?dq zyaxGDwg)df<5i<}ccOD5Uw-`cqL=B}({$^1+1YK!9PlifZlL0QRi=4IWQtX0Ncktt zxThh-mWIS2cC}}LTlBs1Jh%=kHBqi7Xdb^bfA)tZ&|IX^RcAcCaWIBfMb`sR(UlFr zKn>cfWl17h>1Nizqwi0?>1iHGak~}FEB0Q7re!zFe4Wua4~(2T?ue2EzbZpTdM2P# zq`qCyvfsUUL)$eTw;Icrmn_`YS&@!R^b4k-^O&gI2*`1q5t?k*UX`jx=8;`BI6o6W z6$a?3IqZ*RH zmACF{@~y%)5wY@(qGS3XaM{ zJN+67(z%BLEV$dNFQXXetfCt#rH|YpY`{#&mGQ*k0oAB;IS0wcjeof{PMmW_sPWUR zGw->U$KUm#AL5@7K$r{om_?xC0Y3DhdoSinFmL30)gMb~PlLJJsKO=7u0FRHrh(7t ze>|I8+WXRur;+rm^bXt=T`f2=dP7gZ3Rik2u;h!lWwXqi#O+R1d=?9ULVc|6_LFbwkF~vb0D0MKD~4ZY0`%WZ@+v{7zS1p~q9)sOd6u zhxMQg)5RL)SgF#hY2!_R6fRQwc{DgP-#bH=9S3p|Q8y>YQsYTN$?qLH{F2GHVSoK0 z)ypRhj1cG)k$2VifIbem&0t z>qBNM1%aX3#wug6G8}tXvPHeR6ZzFd^Sy^4ZX+V4xRwF=pX?t@Z^kzCn(m`JN_z{Z zv)$CIcxX@^0vO39>UH&1>zwQZqs_Hj?Qh4G;J-IS-a|@tmW_=KRzwb(hFr>mQFRr+Y7be|MCQV?_*7UDc~kP9-H)AL+^d!hcAGzL z@VlLBuCvUjI+L1b#LqY6+DnJ$w`9!imL5jnqRYWkxs;ao<29XyMiN|Pi6$r2OV&zr z-6A_-v9HB;Zov2#H2J1Fc2wV~g9OIK@xDr+EBDS2X?2#_zI5g~H3g$~UOMOj^yFu- zUbq@!kw@XNO-~*kGUjCPQS+Is4Qc+wb4p5JqX;jub?oO->cY#pb-Ci##B<*4Hqw)z zGS(nzzuqFBpi11jqrOxKv{cyNfmE&-c+x^Ka&6b@~ByjDOC%hy$d zW5-s+;_}pYVRZZx;a*`dz9AKG27i^MIS8QCjh8h*@pY-{!kjT3oK(>;ObRlkhOatw zb?ttSl7mCZ7_Z-&Zro&!PPUKRg;3UhNR{yE9$4xwV~{tw18KQG4AP&Zuj>Q`p1p(8 zd403j9r?&rM_gESMy|<(N{j6yv zpw!(n4t1hYQG=FfEqCTT(-J1fi|j$wwpPZOie!ITC}C0Pw=?a9Z|TYO}O#6top^d98ABIX`;sL z<6Pzl?f3xMF;M4-n&ffc)aFU;$=E%wdf$1Ok`$MXhSAp_Rlf)j>QwUZ8qg6&EGGZR zMA#ot^ud|NU*;XFA@WlZ)~I4n=Em+wg%?8uA?Q}nQ(EYkpzB5NM&wthVV}zDhqtbd zKhE(_N#iePG%qx$bBtGWRCb<^vLDxXL@2+lW7%cp>op`TJmsyX;$&$3thltoRV|_t zpQlyAY0>696s@=S*T~8PKM1#qoMXOVT>LrUyA=ojhc+A^OgTbht1bBz4g{=GbY!V-j6Y1A#~OZ(#q-DmTq?Iu7DuLr{`DXUj`l-}RD;q|O{K0^ul zY@Ac=4eXA<%&xH3hppS(dP@Z2=@z-m8{E>-hi?_;w?)SlOT*?97fhV5mj5hNj#z$w z_$k-M@!QHvn|T3uR8MJG$;O4YhY7NzaR%4CIkr*yY%O6ui*Uf*rNK+{p1d_0!QIQ& zPs;L}I(v3&icz||0bQS?oLKU0Ui=)X@1N`$kB|MD{bcg-s*%OLm)?CPA7ZwQ?&L^# zHIAOZ@lG)lCQ?Ufeigu3pPuDc6mO!gfa1h0A#Xo_esMpKw(nQQ8FkNZ!Q40pu+b|> z+2IL%w(2-y&BSw|%{VHhaw)5R{IxclJ$mV$%%hMR_`>qM(^MlB zM}Kqn=fc9iE?sKzYfHC5dNyGqp-c}36&N>{wEPSKA3qv7)ae=VSqv2D8D@=w-6mW- z!&n0X0?>9Lks}@aRCMh9s&~I4W?N{5=7U`FE=sb70M4m%wa#IiNTBYM2gN~J8?{GG z0AwF0#T!9KCa$bW7}gCEXLjZk_D<$v;XU;WlP%m9EL5PhIrko>+YEP|2zAxM!JPXA z7q9!fZC*@lZA5SbC%2TIDw+MCjYJ8$cU8$m)J*=Tfb8u)iE84VHm~{%`S;1A-~TV8 zHzHINe}FU+uGEHVwLhdqN_T9gJ&@a-ppV71nE z%nfr0iK*dNOWoe&0jbAtvYsxM(-kDEQo^5=WjCeY{3sboW$K!r?R$Z&hTWySbR+_M4I&>i37LmJQEz8#`#1 z=|<(WYA^WXRIUw3g6*iYTfJel(uPc?UfR=&FH83PstlgW>fzC|$d72Q#7jRwT~2d{ zD`~%e?k>PQG6{VAB?&6C*owX5iItL*qlLX}7mx0=o|7Z;)kGZu|Gh3$%e znhmbB)@J-$DlO3QiV;)8M!xpqA3=ae1Gcqlfxq_m*nen{B!OPL;E@l+sDMysJ=e}e zr}`wD%Eb@8xxA>6AH!v1ikkM@dS#sY_~ZV~4b~n)zLdU|hu92OVW@ZzQ7RbRiYR72 znbT&2q?IlGNT(lxGm@>MloG`L7He#zSqZ?G+vOuu)QgzK#l^>dKuG{xnvCV&2I1rk zO-(b)dwICKu|A~1HJfT4$O9u-2)>vbINn+L(9MW}O$O-R^{wb~%cqKWh0cy!QF3zw z_X`ZJT7o_8)@E92z+OwthG`m=023mQ_;BsfHU8_2{g|s{N=*}kGT1FBwzuk8GmTqcm8t#Q%w0*^{f`9pJTU!Xk`zsg7runt@|_c(lN zPBY%JD~aJg)_>3Ys*ZMRAA-hxT6^N5@Fb6ZLKummuQHo60XRX^z%HV_|~b|fg6_j;P{=vxM^&w z^Mpm%+qD{~h*8$j?pBNrSD*bzv>V}2fMjhsQ4fjWG#Y5QzBQQi3b^o{GOQO7XdyxB z!Z##xn6h6apO#@xUTO1M2ucS6GKP=Mnw;#^(MigWucWD-3C6R ze3!?a`!s4|dVcLaI`1msfs5m}f8(J@_Q&e@Fr18WFu>AhMd>0)U}~_z*F_#u^Fk{W zGEz_+3Ap46op{h!YiHqB9B@BEIHm(Zb0TNOYa$sdG?eLBkBXYGs1`R7;qK!(Cst%{ zrByNy8F`pcWjuo85RBVR1uW1#=fg9C6V+b`w;^)A7mDfRmHI&sNQcO!Ow2HjF%tG2c^fPQoE|SM#{r=c)P^y#&R(UgmErjDx|uq zC3t<)5hQRtNF#zV=dDI1dV^uKPXvxx!)mFSV&@8i?J)by$Q0J65i8gZm56%laIThF zY&Vpl^u=s_{m%YCFESj0hm_P#9o#~vb@!-f!(et6E+&U z>zQ(pEZGw+NEM*&eGSBZ!HF=#%mke`rFV>mj0Bf3L%P$<_;?%%kv+SF1yC&cm|ag_ zOI9blrjYhu#(85H7bBrWWQqWDOEqffQ>1+#SqXp!OM<9IP}PG~8wty963F32j@q+#_O&&CrF_Go+Zj5c z?3mRAB=WoKik6EO-%BXw0colqwR^cFrmQX&zEZL{G=9_ro6uK(Kbl0h3#97?pg!BR zdK3D?EK*Bs8L34jNv0S>)w|bn7#Jnw8 znW0$kN;;6(^HVFqcDNUF$6N6;>akIQG?QE;Q}nm82{PwM6L4gTT#S5YX|D(Zj=MW8 zHQU~S-G)QuRiBuMwncTCO)19Hyn6N`Okj*?Zsm%!rE%FC=icqqHzMY*F?<9>oc9fV z7sk86KjpJDg+;s!6IaSaWPU*}ABvjT^?Y>?1KbQdFw_Z@fBS^Hu%=?WgQ>k-N=P^B zONIKkuu$&%Y8Pj*7T|z?12f;^B79a~rXP$igmTTS4)7%#*agY%?L@gBJ{wc_YrEL> z3nLtM@jpOKX-+?D7&XMh`mcYm&A%g(VE#!EPu}c6%K3kR0u?anF&W}q{V!li5UI{d z#s*FArXb$(xlWD*mGHkk-wbx|WWu4&guA1=$HaH53x7OugdS>l{}b;2-(ZXk4`90` z#+IAQRkF1&+%A5VQj#xV_%9QNbs@?=JGUwcP4ZmRDgH0O=ig=dzeiW9)qsehDr5TD zKj7y-1Z;u;e;GaSJ=n^d1U3HK56@COX8<#s7QpqaP7flS5ZttNlPpTzZ3>D4YUCxs z0qqCfnbA)F_5RsYWaw~#;!S}+89BT3hn9Uk1%EfswtlrLn>=~TCMO~JE8xHg@3$jW ze&rU-5&9-S+|!Bi6ghe-d|h;J8(kl4kVWs6$O$^ESuH^)E?s$0E&TPla-9UtDM+om z-P-=YP+S;Q#liYfKNZF$#~O?|YIdXLLZ$b~RsJjCt35*wz(Xj% zjO%J*b1_mn{x$|L66BzoeRRY|n~y2L)zn15>pqEX6yVCHC*y_T(Rt{&z9zqN@!b)A$?7jQUu)4 zDnjR0F0uj>9Vmo`Ej#*}In_MAEa9fQdnJuE-jOgaj0D?#Lu|0s-O9Vc4Pp!vzQ#{pShevZy z&Z;VBSRxixj>+zA|43e`BXWXvzX_Q%GL4jr&XWUwta(zCW!hC44c=tfYza@ID>LcJ z8Dxq>wl~4jVn8e$5Favm<)y{Wnikth_a-OOfes?FB@>T#1L5gpYc}g!%Pi}6 zitTr8OA12OmY}6fWv)uJcBv@ofiSwq{t5U?!{v+M< zgc9kpweB_+R{Oy70yW6ZGQuWG3Im9r!`L z=xh;<9ZBkekw+`>oP(DoscMM#bTjEmwkB@{daN;oAGX?YbC-ML=x;iXBKl|{VDd?a z^KZmk=lYZ_B{nPM3U0&)7qi$()dQF;?;ME|G%b~jQutVl(9cH9s?->c7`OIV~qy#n)E?cW?OLO0jLv{;i@@J|l-Jmo<~;B3|SJ7FP0bGL#0EM!z z)L(vCFI--_n3MYzVaEpIw^DU1Ub?NLK_Wv}^KnH@v}S^Me@~ zw{3b+J2WQ0{PmW%h2L=@rEL!SHj*&w;}dP&BR`q1YUsM}*Oa+>6AqJo^`<^$nID2l zMepglM)&*EyXv2S@lsk*#|C2!e62+*vti_Dri(===&WMz1=}0KG!ySEVBW`Spy|;l z>(_6Mnbb`kKReyiUzQM#oyK0XYnv(;^)aVh0Ha{_;S*KmfCZn?seEaqv@kQC+0Dz7 zqB`cBi7J|Tu{N;55ktWJ4v%x!NB|()=T0y8*iU29@F{Y=85F<<+*FMQi0P^eh5lJ zK#kf2q`(>^o6BQ*F@Xmg4fv!&Ta=NKWlQY@>Y;#Np!!YMfsiWf^r}-1xKfqP=(XG1 zkS|C+Bq@BWMC#Z)g7TR9t*}<--IzjJuF*Ehw z!C$YMEs5CnAtBl34`%gWojkhu2>g7n%m)I248BoPQA({SzY?Vu^?V`8pSuz1Z&}x! z;UYu8T9FuSZF-B43#w%2{M4)zpcY`|v=<4n)r~6`_oBTFbsv+`Os<*!5qdmxS?XPi zt3lgyHv)4R^5=q3#LeXvgF8s+H-MP?nc{zi1y-3fz*?9#HjZWUx zE>8wi#oWbe;+Uq)O6_rj8Exz9pNH=wt^bC0IxZk%ltqUEolG{sfWEMpkL(%Xnv$t+ zLPmWL#_*N9OX?4cvyr)c7f@4?FwjipD>Mq=9ByA_IIf>>byI~au)94cSDKn+BmVeS zcW~aIH*}ipN)jq|I;y(w@3+&WuK^+!#NRy!cq&j(JVz8@P>x4CLn}IrGpT6+8r1T< zwuBXo@Mm9P{n5i05Mkwenmh>2Hmo&uy4yBHnJ3i+SdxjoR{cJBJgI zU_SL$Jg2r=DyzG%0-5d;|BK?0UL)d6Ytz`IM{Ag{zi#ya4;*2b& zbCd0@9UK~_-`_-Ix~h1v`UY`5pVXvrp|OdyI- zS(&r8hO@7pHViIG^E)OH-IjWDc6N49--n0qY>$6>G>b@I)X1IYN&#)nqCS6@t=9{+g4IW>$eW|_m+&P&--tW*q!X(^Bu0=~_ zm6%l`!vSxR-pl(9#!g#x11GW>?}A+j8Ckn4FW{^$^M1D)?wTaDBt^*X9hLZbe?*cB zbJ}49QI3=S3vK@S7m$~((2>t{*bjuwve)^bprG?&gYnMOO2KM$I~5Ol{jY8w=A!!R zHl`cU#dfc>J)Xoply)+Vb6aGsZQq;MKf8B5&}kZ71&W`&lFzlp$u#5(mW|pU zjQ2$ZE(#;1p|Dn~A+%=%QDv_dL>x2Nuqg+bAcDD;VCSFnlzZl2_Fya`aFlwVdyCeCx51E!7>XYt{KrEpNgpF}O#Kg1rr8TG`#!GkN zId}yYuuYcHWl!mz8-)pZS-#k;CaaTNU^+ANxK1LJOc+3VjI*!=Dg+|ejuYpzhSq2A zad?6-u&a`mj22+3CZ+_*)*b)wLrU z(3fco-^>J%qn~pL@xzas=1n(1p!#2vltCO)Mj#y|A0eN)p2lPJJ0ca+O}$b_ZD#OTL2l^ zymTV$)=y72rg=gDJt^J3`L#8gAlwY8>va}-d@dd{2O*71(S5j_ZiA!pg5!7+HM4`ZudO{I1BZ8gx!2ml6Xks4NnF28{91j8x8=goTeXMi2)2GQKaL@ zCfw-+m6A?rv4BAn!qlxm$l_uja`Wc<_t+zRXmb!9t^rrSo%3LzzyGzim6+Y=_S#I7yzZML$m1}%Ku={dHzf#TMf)=+$H#kelN~&cY%hvDuPIP5^HCSws0vol; zGpSvq){4E`*?1)b*QKO+&u~tz)e@_A!ATTMa&WD><04#t8_9x{t|VcDH_#JG9yoDm z(U6B@L4F7X2wdwuH{2p<;-Tu;3n7tFZWFvmCSI&x5m7jg<(wh+%qq(}S03Kq`P_&w z6aGZb@m_#EjNMLt{yet3j5ZASfV`r9(xVFDCr4xiw_@yF#76+rWo{AXm;SK%A~&x- zK?|2?zsikTJ)e#Tn-Z;U2@}qt$LBI}JQu~#MaeMPRKZ=~jdeACcGdd(3XqZh9<9#E zVeITO_V`he$h=}a|CzNL>H0*j?__d#0Cji5_t^Uvdze+Tg(GyceS6Vi6tR|lVQeLY za`f`eu|S0&+7axaYUm!K!L`CYE|6`y(r8V>Z9bzDDqM}K&UMdA4!(`Fa_K|oy6CQ; zx^?-jKygWxf!oF?zCd!bV~!$r4OL-;Nomb@L`Q9BsMVleR2apv5ga@pjIsQ)v^gwq zBiCW~hht-vH#z|FisJT@IehrYdZujdcoGjc@yO`qyXw%*Fkerlz-^k4{Uo&`_QT{A zaJqKo})z~EK z;sLRfey{aOyL}!;E-tu(_G4Grh4sZC9^?rbM$6T=&IZ z!!3Ptak_DG&{3O_JT<-0xlYRT6E0oyQ6#^TFxAyqop*&_QSrW#-3B?QUCAd_ z)!OUNVO^_-^sf~CSXQM4y;%OfR0lRA^X(A;ughms=*eK=2Cf>F3O1|1h@4+Wcc%t3 zd97}2Smj?nw6Y0W5a;G!4|=NJ%W=%5EBbpX!F;g6l?-Q&h!~=S-@zDXDhkYpk*@}f zHT@)Eb7=WLz91lcCg?3nM8`f9o9?NC;-bqH&Z*xy4d9~)8*8b~NaFYI{yA!qxbex6 zABou&)B7F>LsZKj$eBwiBO{Zia6=sNNL+!!vm@kt*KF|aub4&)IJ6Kk=uEj%)G?&y zjrX)<$!A^1R*s7ivPYV0P>~+5N7QyJ_^V4QBa>Q?wm3VQC2X~DisGq=Ie@VmCWbC~ z+JAs;E@d@LBGY+8dLh;LUh7uwW$sND>j*jK6fo%gn_xw96#7vO>ngBVZ<$Qn2O8=? z{yq8YaE@!~cH%j#%j5TV>E@A1=3c){P4IlSq89YV3C+%u%fo(A1Nm#@9P2_WD2DWL~p*eO9;}%m&&WFDK3RFeEr%)j1JSu-8%4M8Ve* zCa%MDl4X22%dS>Ar1^`G%hMTII*n_3uH&Qb#?y*M9T$+bUw&vBN*qtGM}S|4!v4ab zte)Lml0rSB0Zgw(u>N$d-F~|6J?GeB`MRf(ZAj|%d%yxmZgxAO3Q_>bDao);%bmhf zY?1?q61i25mt>3oHA~XS0Ur4SUZuiwK~Fy@I(!I*3S(e#Z+uS{&pF*KwD9CF%?YCXQwtggcHhU{IygDQ{Sk`5w+b0%>l%jtfnZdc%p) z18Jsvn74Y~Vp#m$s(&QozNkC8g6psQD|mGnKD|@aDpzhDJ?9eDm3yUQz-x7dvyRv_NZy4TW)W{vL`>atXvXZ zBqZlLA=L)Bb3H*V4m{w#pii;^Sq^}|J1X}u*f7;lzdgltuWM&J$gLlaVA)Y|-&riB zLX)f#vgp0xs8gWI8a6))RAn7j_B}&+0lQQut#!GDdL@u1+}1{#6NAg>VxG4&ze8UQ zOU!aNqS1FE@coko>{k<)m;@4DK8a=Ok=%mh)gOdd)TpAv0O_mhDj-co4{6x}OQ6*j zf(8PVLrT|yYf^^JV_-`Irq_UzL*qUc(<2-sm8KQ@h2qE*lj2+elRtoFxgGdFwkxCo zHc%R|81NGC-LuMTI9LVPe>N3MdzwYA)mbkFm<`Os%HZt1nVT)5ix^c(LPg8rmXJAA_><)$L(Te z8})V*%9TrVSAcO+TiaQm+Y!1_EMvR5&}4;dRY&M!HegWPJ+hVSo}!7|06@Cyx+qXv z6V^hqG|~1t?i9hh%quYoT!k15uh{yQj${gDSQP?YR+fVMNF(( z3Rz)NBvS@|oPPlMd8aIMD-njYmF)pN+R5Vstzz}Pw$0|?5ORg!0#d0u8VAipDwess2xUKiAtw7BXv_J`X>x2}Od%*Boi z1mi~MK32X1#7im^u3iJmq$C!|gB7ff2Cvsn;OOY+LYkL-Z%BoVotGzZ z=(x~;J+;Vwv|Obde0-0=tN`YUQ-0unqUPrs?y6=GsmD`Zc>Of#=!4R>wy32D^wii6 zCdL;(bD&KKm^QGwi(IAFEu=(rxx>2=eF!+g7bkf}Ax8LDdjNnb01zb7A>9*B)V!>$4bnNkMw{#3Xbo|d$~@-2DAVdB|I#$`(r z!M;KUEB;W5_Bat809Hy(}h+KUT6bw>U*#Yb6T+LONGkJEaw@s00_^k_y=wov_1oxWa`8 z!xTofxJ1{o;1NTBc&Jrv|GMDagjHni+ThYG_8J?6mRVcVtKa|?IWZ`$%SOKfp>Fy+wmrw3NqlvZRIJV1U!s6NLvh^O(68)3|0 zQmB|*Cu+r4YmV7bUR`lHuYS+wcLFh$jX`}N&a{NO7+tk$px1UiyNnH`e8`W|e>f5T zL@WkN1kt6Nax1lm>zL@c>XlOQkvm6CrZJML+owf-A?yYnFS4e(HTEg{Q?ID{m>^y<4c z4G9%{Sp6H$9Cm2wGhQM0e_Z^B_v}Edc%2_OfBrxc^jsr>OxaX@05rIfo|HH~Y(%t4 z>2@Q|n6i-biocmCH^T9HT-xz%uFi8t$u)~r~4!I^A5!IdF0}1 zSyL?rvu@4LN_nbRd5|X5ZVjP?s3T#YxW-IR*2*kcNJ78fyD9FL1KL8`vUD1itP<#M zs2y}8wy1dH9A+p_Gdik&82BaZMVjQbu&{FhK5Q;o$xW+d-SDIYL}5X+4!i{^LdaFH zJ{P0SIJrfr!Eh9@MdVlc$htr+0yc1ML*U56{M%UT*!M|>4D%T>GF^zC_MeBZ#-o?8 zOVQe4ABUd9=2jMTkW$bzKeE9LbGC52aRoc0Wz{fF;#aw5E|abfcb zpjxG$$I5OkkeAf)tGn9E)ysw0@yuweQFfuxLy57XE1@JMDXM4-(Iubpgqvd(cUtGH zCVqx35kR67mBl13%zTLv&t&cVE}PBzu5jM17Gbj-w2irlyTFTHNw1V~w1!%cX_tLr?{7~`7%RZaSr%tAG=iPpCiAjWwy+qk6WW-qVh@@&>L z{1tNN*X1)5S1A6+_5+hfM+4Cb8pok?`(8;*R%RamDj(gV_;aSKf6mO4``)zST7H}j z&CLOX9k+71XET5DSu!W|kN7{UiJ5569}}cCABA~L%z@kP&f2QD30$auNY>9)!_Eit z_F>-q{f*V4!kSR~c_izOob>QIp|$NJ6H6}Bt< z$%ZKT=ulzSNp(ek?V^hDwc~d+Wj2B6G4Qpu_h;RK*)l!p*VllE0IQ)dtaBE16 z({@Vl8nrCAv0lG2Uq zLBBHIN&?2GyBV5MUi0`J_$mGz&nAe6eL!M~v~;bT(ea)#qo{*OKv#1>T`|G0u7p#% z;bIqJMUo1Sv2t{@Q{E%;pG&sz&}vgMPW9)ra$o=I&sg%s8o1YeZj8flhCx%&aIn}9 z=@t%p8vVbF>Mt}ZggDhbw^u-S>GJl)a|-h-)8`Ld?$g@y>)M!QME^X8h z{mXjlzw|E>=ir2b*Xz#Cg#XVxl#D0-F-NjillHsF#jwk8Xg;#cO-uMIpKonmRiAe; zDq;KU*ZF-RA8jx-xu&71fkXRHN$%xyy4kPf<6TV^jFYGshv?VL{Q+8uWUCe2{Ks_3 zEJD*fK#M*NAC?emNGri_?75?Ekl-sG}6-FGS~86N4aK*&{AAY3kHn zr2-oK+-phtVLnPf`tvL$TR7Nou(cQZ!%@sz0_{Hrw> zjCQxY`0he{1-YwE@;Ax&kM;F6A+&skR&(c?y$z7H`FT!*21r4+1+0fv+=nnpg@L*A zZ{YjM^z(>vQ#VlBbFp(@NrTyJ;`=rrGN}nN5W8Er1aCKPMX3Falm1EVC98?6?-gS; zPz$EcmEc+4yl7X#_;ae8fYf}ItCiVb5naXx$P|D$0@@}Flg*5J*Ik5}MRNLJ=?^U0Q$;lKTZz^f+_xdEaw>zxR3WbN^De`R=mz+G~B*+H0+S zGuVY1$CLTCCZs)iiUKo#gReRX=9#)ZbeLr1bb9PoUjpXWGS|Uv`SB6AA{^VD!~#c& zHZ9`zT|9RrwA6q~9J9!rnSMX3BH}FIlt=2XOq~AZ>IS0wGE?uysu(YtzqA(4+{PEt z9}~GCQCgi7tJ&|u9wK|)_;PT@QOY?Rum^5*lymg7a8ZzZPFAd>S&xm&{gF5}N9NTk zA8N0H<@#vn|IU(m&f0xU={vFqf>h2>M?u16cgFbB>JllkVl$Iig1XM_D?L{&J3@C- zTIzecU;A8tbNQ!XB5Xv+-ttfT)VE%In5GQ;PC=PR_7zGK@G}W#YsZKYKNuU)D}6$O zSH4?ioDW8#p4ZyU6l>X#QC4KN^130;7?rDle%b7KVyc(>%48Ssnb?@`X)g>uZ^VlP z#kUT$9+c%(|4xoLQwxN9k@Ie+Pm~2VSPpGM@b7@(H+;PbF8{*~zzrM!Cd%9r;p{-( z)_TnEmZ10?1pIF`Y~k5|Z=~Pcsd40Hd{s)yT3VC2+3Ilz+bcgxc;Hv`q^d#Ssg#d-Cj5+>T#qmYi=abBe}-4;S1lH;K>oE^ec>R)^&1@6aS zFdjB8jU69eTtbW<&Vo?N;CJs@ufFafbvS(#Amj2BV!d1YG514<-g!gAaN>k7qaH#b3Kcy@Cju;Dp8*x+P&y)#9#a1b=L_o(2U39?^kWFA5YR)9I-%L z+zN;KqCO>WfW&gkQTNq5z05uhdII+3k4N^WjUx)|Mf&V?8_PTcb<06h!KPEqb?~jGXsKPM+CzIe>`^TUj{LKKK>`ZWUzKy}NMhn!qj)+#r0_2e z3Xlo?7q-O@JNfbz@-ba@rTz3x4Ck}nj{YaB{nVfzi3#Md5I9_^t!Fw&Mtt(>3R@AB zUyYpMb2}}bwM+k~?S2^ZKhaQ%n!0KdTfO&N3J3R9CLTle_9~uLs#p)%Gt>UnQax5< zJD+VysQHicDiyZ}46UAE@@mL_aE-Z^?_0tZAQ|2z_&b)6GV{{<2T1GakGt@TAI9m@ zk9y#1meLnS{BJa@llw~?=2wHrd^1I9i-CUNsQ;mczhvZ%)VFUb`NL`ZZ!`e6z=*)j zkmN0ss%kU83y9$OV)3N80BXL^7yg)YXTYy8k1l8)wew3T!4~;~gP>)1^jn@A&b_;^ zu6q26PPoP&?t!H#AC!iKJbT%Q<%I zK%X}C7kEmq59#mE$w!Y6Sm5I)Q%HS=v)CH1uMyT?Aq79mz9x$Dm@APmpT~83C@%R20`thKwq>#6F9~P5$UFqoR~D@xrYi4qsk_x_3nf z??fI@S|v9S5X03oEN4cK06d<^AqM|}INDht(%B`hK!GLqjzcQ=augh!%VlqT2ebA# zsfC+uR^|L6nXkoftXss4-V{hO?fWBtEJjau)$%V`Aswi6pgV2XqE!(y(5IrLRN8a% z4@c5=mAe=d`t3b(>`IpwH7e9{W&3|!}hm7QnbMR{e`zErQ*u#Bn~>& zr4TTZYI%GnssrWv|2hr z2b!up$5!MJOLe}rnq}0t!vw_I{qS@-$(;`q9(~^dqX!?SuRNlN+|5A~R#Citz7GpV z;L#t8d_};1!;5Nc(AXB*)4=d=#opVycxlH$vW71_^u%s~gNJ&1jO5fBg7MPRa0=p+ z_nh)Ur;1MxlfB%|EH}$b&3=bA0IRfyXi~=U){HMYR_Y<~!H-8ejTbE5f-ps(t!qq| zL+xA(zdKgizF;0=h*noScyEpD5wgDy2mIi^EJa^GMH~3-O{q+QqV$${v?fnlR-{{ZO zO8yOB&bD9H0ngOprpi3JZjG7j0tz4fv1`41y2KUW@9Tw#PQ|R zZQE|Gf4Dvzz@~yORK9g1WPLo~gAL@cKF@92UVoV-Pzd?gb-RG({kPp8A6!_O@R*@s z;eCwul5Nj*fZg4_&PTxdx7|c&CJ*?2y8H%O6QPwnAj3#`*cbUn%+h(E$-&BUCBKAL z*U`w@t3&mQkmh&v`)B#-snd3zbAO~oX~}JvLmQpgX(p50KSe!+&a?H(7k#pnmPDEO zJbMzc=lYD4n>Jx;Dpc~7c2Dm>1jHQ_8T8b9%v ze9$4KVQ7hd@xT>(n8CN=?qt__P32;iI_&azs*sjJw_6Hm2W~WZNhvnZ=HmF-w#ts9 zO(TaIuueuKo5z74c!y z3>{t-kavgvFv@A5%aVpw0g&2W8y4yt15&qUQvjeQy!xwFmIlXS_> zk2N@gC261FS(Fb}^V-XfBIJcKC5z!a*b+1kMC^p`URz;<^4}jyd-UvCm4P^Lt9ek{ zZ^RAjajy=Mo!MZq-)d8Mt;N(4AbjlCir)nODZNXOJ!xf3s3)~_7Q>j{Rdd4iMCb{% zM#Z4Jk3`Gb&m?Jk9Cd#74E~#qnaGpO2O2B2C*33F_WDKT-h2k4tnfV0?+4UgPEjD~ zMpN%gXH6ezlQQ$O=bYZa5Q06}mO9sf>)@xaM_)tT3Uny`nM zJMor{Pe8zwe5k?wVr&%)DG>zBu{X&ipZ~G2V8CA*GxWO;*PJ$K`xFqe&o)A zx&jH!lm`a?&e!ShJEat`s9Y*)Kt5vG#eu0xOUT|Psvk1t@Kj$K`nSG^fK=A249hYKKcwh)@ zBH_=vRa}t2;R9<_SwzRQLVev7YX6Op=eTa3x!O6cvrW2yc-e?QP`{1q0d7fuMmu*IfaXem5;EAfu`$W*;&rK69*m z&K0N>o33ijrJL+r?Rv~VMONOuzDG^{iBJ%^^7|tnufdD#;+phAc^zSs_ZnG`4Xl*F zU4y2_o`MlM`!gyquU@#FP8cKx?i1$B7&!%*JbSkX8Xm`IgW?*)N7B`Te=CUEh1oq8 zq zg1)sB#iV7rZnED;ZHvZayvV%bFn<^CfwFpHSqn{h{?i_5)Fh%~=0)k;-BagpT)WO| zPt`$a$#ycE3B1Z4gE1s?tRsC^Vo@%{9^-~Fys$f0i_ z*9nx5z`7g!Gl=?%YqnhgGL1K(;eQ2kWhfF7*gls1yzSM8U%#yBZ@an*xEzK)BTNAD zJ^X?%|0RI9{hRIq1`FO`Fn$0D9_9E-|E~b?ACbfY(R+LV=9Bu2LKE~l!q{6Kwrx98 z{~1p@>u4*AU%~#g?bV6RzSm-S4<20Z9X$`Tc_3Ps?f7ypP(?KA4p4;|T+Lm?n#{Q@ zeZD{+tXAEHs9+IV&Oz00e8P0Pu_hri@LHJ4(M2l>u|#^K{AxrnmlC3XB(41XovS|d zuj3v(@3R|q^L8MOUeMavx!5S(QfFqw50uxLE*<8|87}8X9nr+Gy|}av?Bgh_qH)dAm+vs<>TT2>9Jra6UDnLC zT_wTWs1HcsUwwc_L+Moqpv^Y)d;_-23`2SVai+i`{ak?K=VcFLD(!$hPzNOLPoUc4 zg=3ww&Q^oE$@FK6f9wEk@}CSLG9Grm#*3 zUvNgdQ+NA)dgyUhn@MKPJ2vEPFQbpWZj4JZcXxMJo~_u zhIzqwUQ&14*pO49UB-s>8Wfm zt<;yoY2*)7uB(J!QbqXy%%X{qhW4B*IO6F6yqSTLR-%7QE0x;zs`yq*3S2X`Cwx<& z7VmG!0Uu{~eAPX;--xFouTT_++uH**NY}uft_!2)He}~76;vb$j7CSYU6pfVo2W2| zQr=gRW3vl$Qu;hzd%VKeJlzP@i`*d+O&^2iUZ7mUs=K5po;;wKkWdDf?6Q(rdml_| zhkJB#ok#{a>7?A+!}w=FT^=rO%C(Y(S4BsWR?&@@Y&4>%D}~dLk-#EurOku3%+IlI z?}hUynj6(1`*L>~dD42U^&jX&f-I||44=+r?@9uxm$(k6*@$^ObD^dlGfeS}9DP1c zM0A20#)$&9eEuNHovHe}+FUuU{TcUC7)?rE>Lb%!dyEwKiXyCxLTIVmRq{^I8RH+4sm^*g{1Zr`(8+rpD{bnRWkhj;6G`ZwxjH$ zt#b5lLGG%BDT6&^rY>c**4`UV&%d0lX~@~>W~I2-9we`BVBu%$M8ALu<3H7iq$W)1 zu@%`rPKYcRA9~#=-I!|wo?4V}*FQ2=Wv-q9f}}^e%E=ft$``%sine9|>o2J>89)40 z+AItB5TpWy*V#8F$1^783AE%~PGMwR>S=b&mD2+V*4ofbQw?kFbmQNz9(Kq4DHtS9 zIcUZKqgv)rNRv!Y0{A11TM{W78o|^@i)fLt5pgIH|FQY?!qzppJjq^xm*77GnJCuN z;*UxTJAoj1W4+hN9kVtCv5`K9>kvCT6Tvf&2s<1j4I;G0@L zRwyI6^Uxm2*5YB!?aikc&ZgXZEX2`c56CW`fB#j^``O=1_rp3deplxaIUqw?j11Cr zb#~)F$8%HI2_-&P9l9)W_$%Evbs8YePtjem2U$agLop^==CNzXLh{ z;)Vl=4}cy2F~kRq`gcCOZ}}h)G>`K=5%$@;_wE1upSKWj+5yEdH=T9>m<$9-00?h? z>pH^T_B+6m>w-=2zwR9Tm*)M=?5>%VZFtPr-G0C{Hig&bW_$yvzwu%I%_@Prf{j?Y z&j)AY`t^U~!~CyK^Kaavd%^vo|67dw@3T)1cD*DKVAF1FOwIVi-GKi%>hqRcv{tnM zwE6PSzoX3vXy%*Et(j}i1L$nH?r2`;GrZYnKl6W8;QY-|`=2_=6@1_D^Z#R{_1l4e z*Ye!pkN?s+{F{UFH`f%y#3nnw&C-TI*2ZV1ep5OZ#K)79Zcx{2rIDyyxdwk6z{LUD z84y6DEz$1DipA$3Pj41s_l??s2<{zdH-V%n z>TTW~ewJrvP!)LJP-ENQW!#~GLIMZJ2gs%>5^n^24k5mln=Sw53Lf+D`XayztJ?#2<&!HWJ=G3$psdA>0j}I%>Cp zfP}i4cg-|^6K%G7VA$OFKErtOAXajM7o`OEgAd#v986(OzZMwD$(oQ=nSebYziw1-ztqqS%?cP@xKP~%!$B>kj`-iwKCwrj9lI@sASYZaGSN=f z5y}eg{M}s%tj@h_&87D>E~;cqZNxu(<%fZMhIdJa)Cq#BRI!Y8C;g!ykPI``fbNo_ zj#Kj>>5fu+1T!1xi;WDPT?$!SW2UQ1;Tux_^s0vmK?d?{WL0Eu3t3q*_6DY8U<6}{ z6}a}Zl`o4}|5z~*Ah>8~I(|MUw@k{cH0p$>uXsf|Y4lTc&8%x;0J1lnroC?N)3Lb= zi9B+j>xdpufabduhC&l14O!wkFWFn2m``XPN z;oS)&L$V>VPi)rB`#OEEPEPesorhUj4%79%w|YOlGbgOQmXF+&B}#4GZbILW;tB;y zA6lB%gu}g8m$*1%Z;d?Ke)%$d6%Hp$*T!$(jF9^*6>5;t68!0)@O|HRF;}QMX4b8^ zvKgfCl}prl#Q*qO74d5;P-A1O{^3^+K{fy)_RGcYEfX)OTaoejhkrWU(~i5>LMHr-j2BTxqKmPUr)Gz&?dp!s~ z{|=`i=I*)~9`==G2{0}6kH0k~Rl{nY0v_*8*fLC1l)bl33Dow30$aPc)HP+B6}jC> z^a)T>^Xp7ioZEMHY?RRbPR}IyK3xCtMr6m=F3O71)PJ0lTo+pB$F+i@#lb(e%9#+Z zZ1fPCG3~pX)#>0M9ZcM{E9~n6(Z=U9T&PJ&NrU?fv-z$DkII!b+Ty0%v{ZOf8^j(H zd_-%dA47Eg&Cd7QPZaa}UB&cuw)sReuus%z$>;7}VZtrzrVUG-3a`roucNFsl~1~k z<7g@o_60sG&W>hMfm=jsI3Qu5&N*DzAdZ_Of~MxE(Pnt~lB4#AwOxfrb9C-vZ^&fX zN57e62yv%1XdSLB%N0K$?=ploh%SN}EzN!Kv;=#sdZQ)}$K9;ilB?u^UrRc+0q+y1 zia{_OoSY?CY{T3l33#<)0Du4febrzdD152}PMdtHFY*j1W1PLXu%MR>M5*n+V?YrL zk7~Cvb4zS6Xh$Zm6!s`;JDYf&-r6ihQpwBout(ff%WVH!OVfRMd3ndHeSLj_N>~dt z8Zmo6x$2I3dO47GtF0Fu&v1?GxKJ3{-fLSv_w*Q8=Qh_>ol8QH&)fMl1SE&jQx^;F z{xs4Q|JHZs&YgUGe6T69mA>H$bzzUFu$6Q74_zZ{2HOFUqDAhh39I?<3SbhrRh*UxvtL69*MvlG+K^uu@J!u_ysq4 z*7#moP7ctd#byOt0crGT{Bu{3_^Zoednbqh_qqs-xfNrv!M_CmPSIaYba9kvLP2rP zR<5pFx*P|Gy-bhV1{P}nVlD$B)MA3Cq+_ok7!!GlPN!e-?>o$4^yJbp<((F9+174{ z0_9r5!om_2VO(5Xqvrh*b_;$&$7+~?;37Ael4M6;P^4i+%0tur97+#-&Lsxbah?K zmUwvc5Zpr)n`|U zTcCO$+}k_%+~a?e`Dm_Xe!1X}b5UZDTsC$bY{t>S;mDyw;}a7_X2(br3MfZROf2a- zCGY+}Y0194a}SUIlGAX!dTMH_&<7}H41^{*nVXvfwMIy$@TnwaxTQXuRpi0>_wUWq zQ$;=f(z4(KZxHSfN@J?)r3YJ-uM}M439MaTC7v`i*B~)a314!aQxsgksM=4?(<#zf zubWqIWk7LAhSLl7+*|n+9qx6Q*PFytYeX!m`**!*>26b_je6L$LL(wx+zA7ouE0Q= zE=~V_oxP>EGXgyscj(-4JJ(W%_THO;l*ELNugAc3pcyy@X{ni+!m+j~z{S`>v7~_) zw>N96%9kfZTR6!$6_n-q(^ril(b%MOrlQo; zI;e9fMq_j+KV`6g1ec^hqgpr8PeE5=txa~Ac(r}uni?bp62EDP?N@a#tCwi8{soMm z$S*J!ti9^5n}fL%X5wFn^06d<>XRNm<#QK`Jh}ydF_`Nc>P|y@qYkKKsjK=8x3^YH z2g+Slhlv@kg`XM+aR{t%&rPX#7^tt(doVvX4Qorh91*$4n@&I?$6Ym@WCsl9#jygY@wNV|q{-oZslfWAnKG|Br z`{1a_Cs4gC?x!OH+^sdTcLlT#p&##oC@9W$*Fxhr@t<*!kQ#o z(ow$|>;Ad*nu*t_9$;Ntelx{B#nY>y6SJG?^j{%sKgQ+Zk65N3?-ltMtp!%|2tM26 zX$>N4wZ9#E^!uf{;t=3vK^$C}B{(=Mermnxw^-ThBj)yF3yknbwYcZ&Eypa$)upc1 z^QT)_*E}oOZ)|*;p#iAAj^=rWgwm)0c?4O_GxNYZc6J49x;z!{gr6M=G^;FreiyWh zD5hdU`=o^`Pk-sNu+p!;wB{UOb`9v`$*$&kc7DHi!VO%A7Etb~8YIqu zmQC*0~WKfjPa64r0^bBFGDYO`RvJ8_*T5XRP-~pI^zb1{Sqq zq2j^)+5+H+8iN+rRZTB#Caq<_XUqm$J~Lyco_Bt^bDtCQBcU+scFy1&N`Od=Tw6Ht*XF+-~GY+gV0aNDVcO?Mz(`}Us>H&KiN zgx|#q5N~edC_dV3dCl(eX@OR0lv2K1@F;?J<-@*kpNWy)@rQz;r!w;ZxKvR$p0U%^ zHK=#t)c_?=xCO~h#ix26D3%}f8?8| z5I@?h*<>m+ygq#Q5v{Awtn6IOF6Oq^I9Yu0(r>%2 zTcIk}GSRkFhMo4+kjGSqF>9^0;twj5!2^e+xNh+*aO;eRH{Wkl*2QDI&p zyld~P#0ck@6gku7$I*^HlLsCXR*Ie-j=!T-;W{*n4jEzHyLQO$lVatPBWpz$T{+8` zJ#eRPYJq@&4S`v`=8h*;mTKYwKFe3HN;IRpf5^6Qov)BjV*&XFzEgj&mbmJb-9+Jg zz04mz`h9N{TP<>4q%y6d>=(j6qJ8b^jvQYz245e}+8@|guYPhSUfgr)77Cr;H$jEdO{#M_ljm>!|IXYiFHbnUXy7bxdTDFr)dlcMH}e(d$odA z?g|nm15Dt#=FWxJ@p#@<6yue;2j=Q|Ds<(i_Kb^5H~5?#6>J7=5}CIajb%krXKVsn z_Is=J?`Q&E)=739KqvVwa?Up$WX%z2sjNLu7T!mPye1=ZPO|RqbJfc0jk+;TYu}qC z2rG?XJuv#dV|0`A!dp99vwK4pvPU2;Z=X+(jif2Y9Wu|>5M&2wJ+A*Wb{5! z3=N6A$z@wlur_iH@2K1*#G_9ivOIOixx!B0GqLiHnzPlskYh`JZ&s96>-MY+&}g!M z?`83}kO!F(2qDbV*TK3j7}mm-s<%EhFwXO_ZZK zEHcoRL06+$0|Mt`@*0jm4-Cwn$XCgaN$9T(2bif|-NlmV8VU##y&BJ|34-;+{ z=!YkRa89Z#D}n^S;b@iRodn~(UOaBTl4EF^pR*j~eA#Nz$E5m!4`Yhb;HHY{kU5V< z-A}g1QyD})VLw*J3MQx*JKQACq{kbvc3M^+X6n=3i5#y8D;Y;ZNSEB)45o?f_$7J+ zYxO{V2-ng$t@0sjb$4u0^5sJ(9zA)#tb_C}k;6xLx2k70X1tEh@@W)r-uog9Dz0r5 zaqdw?7gbYAp%S2{&|H{Bf3KTFd`8bR&y^%*?=^ukAQ3+IwA@45=-+A0bZ$h?3qbkiRfsLCS;d^%sgFAYrfg- zH`@Qe+Gk9Tzz`nhcx>h~Ty2L|alLoe!a@A@(O6+2VaDs(Ac!og!g|T0g+-(aYOy{p zsjyz6`Wbbs)gkL5f^>5b`eR0?87@w;;dNckxND7p1hp2~cR1wIMTwWOj>iZ}{V1Oy z7-4^4@qqChd7_1%RU4v}ck;SBPES~~@^DO2_6dk?Vz&??GSf-;m`%z;gVkG`Wy%1x zqrG%)d+pSPl34wO#%E{D)+Eazr(|xgRZgie`vT1f6@!ry{3^4Lhg-;s<8W6&Aj5}^ zA3W|#b!$L}v6zc$5#ivZRJSt`RLcxjlj`LLK{)_(a03;;`aqW63Ig+Url+p^*Y~S) zJ@cz1R{B^GmJb|xUHP_x(GF%OXDMZfP%aIs-yMm6CQ=_d_TjkGgYwQ)_c_7m>9;)& z_u;}rVR>xmB5Rat&=|kobm1rs8AnZOYMTu+^hr6bIlZS|B)v7Q^!yVN$I`->D^vS` zX#&xLMVeKqoU7B)s$i^=1g`a`?Pj$bsu~>^jvA{5`$|w!8fr`D`uh}>SRh_$6oY7{ zGI9O`Sp2FXt6#)^C=rnyLGnq62%9ACpvRjgR-hP_0ZxhXvo#apk9=jWWK*n43&*Ow zAMfu~!dO$_xc62sKY9@T$__(c1QX~r4H9^I-7LcI!rX#Noz1mj2QA?om1llvvo&p( z2(1}j#M%Og;IpWonB@u_G6Id9f-9Vob?++_@JuOXy{Q@|I46%s`XW{?BVrKMzwSEr zA_A}v{QY8&c-atN?wcf1cWe8TDtlM;2JbK2)Dd=44-&uhRB+_@Vq!OU`Ulg&+2$9{ zopyveB)d+&%&-yHjaI=!^SY6Wks*=M8f7&_NqEZ@X|LF3N#gvm7 z5|C-;%>WnLk7P8LTIHrD_=K@w;VP5dLVK!C%@;8DN}?+4CTet-P>cJ|2qOP1td98@ zcuBGe4M3ylHeHEAXqhM1RVl*jm7IK>Y;OEd7bt1d`WAgYCwGpPo@(>Tv#G> zU>Pf%#Oie7S78qQx;7rJ{Q)k=8VX(bh3ezDQme*HH$NXxqhttgX>bR5hX}yORt7Q% z=h9vwwbrxY<|aJ{M0N3iV$TvqmbrFk#x>^X-q4*~>WI5Uii49*`OQkee^a15*>|eB zCCR(h#s&3sAzphrU509@Bc^~&T@qCo)!CZ?zUeW04^f=_O61RqthQDvQS zW4(6x>)K04j(cQL-Yjai!=}m-J^LMHu*D}~IPzYI3ZdjfgB7=+uvtmX+d#xxO(57* zd7*9|b!J5@Le6icJ$DAG8J6VtVyyR6e8fz#IPyT_glbi-(@Cp!8Ovr7^6r=f(x(2J zgs|k^$gBEN4NpS;IIT(6sU=S7EDR;P|H%mRcQw$~nNjqs9%?W+S>cROTT_WvM`=Qu{w<0sd2!@*^5KHyInt1j&IO`lrv>^+nb3?lA zfWpLsaGJ~7__7_LtW|>ZnmLTt77(bIBVs;0KsplbKs>oVq%ng zZEp_(y7aWY<=p5qG3W%UU$U*`>3$$OqP`ZF;qNs#3m%YXau-wzsC=3jWATxsxmYKb zWZLurMhqj+8V2wy8HwX!2s6dm<&S>P=V$^4nAJX4v%NEc`4|Z;3vBL z4NPou-O?#MtMn$%VZ~dF!6hdpR-X2`ZiHFc%+!qh)U!pg9EdC|p$OYlbYbt_nYc}B z?srNgf}PoZ5D}{|bg+HRB}?lvfa5uM+hI*fz3+)Hz-m7F@Ap zveLzy$uwh8!>>FG1;Mc51Nf};%$zbihs$d7+2tqM$#Dh_eeVj&a;9qfn|AJmRl*Rg zeyCzOsiYWfRGD7nyE@X$2V3Nr?&%-ETGe(nL;4Zsp3X2q9p8*BQs8p5>F#1TN)0m+vWjuy z{Yb%M&DwDATFjJkJjSu-U3<~3(J(Oz)**s`^M=bh7)tcy-|~gQaPn*Puo2p##)KlN z7;RQ`>+)*Aw0pcPY9PPBw*k}KL^*d(4uf$&o9AfM+O0z(cXoG`WLFm9i|q7UqDK1r z7vVJfu?b3PB^Fm%lvN3LaH}1!!EkF#jFTJ;+lw7lEhgr|n(PiiqGd4R4yI;UD>x;f z$&NNPKTY!5>6BIZb(Nqed&n5aHDafjI#^cBxDR7LMdxl@aM}a9Qeu&V8v*AryL0Gj*V{nT$ej%-jN&<3Q|_yX%bq~g$xy2%z=Qr z(5ApMB2+R4>5$0Tr`)8h*yVmt?%qAwg(-4JQJFs;JXtZ0LMD0KD{<`YJ!Uk}*G4`Gz3t^z8`Kq6PD9Zb z`*O&NhvXb=`3_COXYMPn;bfi0ZTsJ~_7>jJpC1oc6cfv{i;Dxxbq(bEIK0Wu&<7+A z80KCKgL&L5&a<;Irj)vN7OJZAn7Q>0<)Cd$@b+U5CU{JhVYBWeakC1~MNao7PR@87 zPVSxu<}BL52#2XGarcF&LmJ3kBPC55c5$TKryjD7ANwl`;6;q7X>xC8S&GFP-91mN z$?hBpJ441_=IYCL_0PR=3vSm?c#Hv; zS}R0~sT-i6g_ufwS&56UTJT|qv4{z9SDqm*qs%Mxu-DXhO=k{RE)QCS$+8LEk13JC zq9A>}rUUp}?yEH!Bh8(ClrE?KW8q~M!(Av&NEgh>VWz(g?_~#@X?6e{*M0a(YZB@R z&SR0bxH#S0gL4BrArNK=1Zx_PKSIGSIu78kn@W($avo0I6)tJHjx%FD1r8J9A~Tb{ zc&~ZX5k-#~av6NI8LH^Ly6VyJprfY;XE7Q!1=LzwiZQ@UPxo~Y?Al+2LYAhc`q~M; z6C)@wJ{-oOzryNG&Enjlb_^;f&0?jH3N}$#dJx<%?d953;cp7)geQC4rYG68ROS<~ tgyCY=su-&U!Du;6WX%#7tt^4?vl5bFC(kDXQA69Vt7=|BT{3_0zW^+4650R& literal 0 HcmV?d00001 diff --git a/doc/make/emscripten.md b/doc/make/emscripten.md index 8181b822a2..36c764b2f7 100644 --- a/doc/make/emscripten.md +++ b/doc/make/emscripten.md @@ -1,5 +1,4 @@ -Compiling lean.js via Emscripten --------------------------------- +# Compiling lean.js via Emscripten First install Emscripten via your distribution's package manager or [download and install it](https://kripken.github.io/emscripten-site/docs/getting_started/downloads.html) yourself. Then build asm.js and WebAssembly binaries using diff --git a/doc/make/index.md b/doc/make/index.md index 21679c96d2..63984f2cf7 100644 --- a/doc/make/index.md +++ b/doc/make/index.md @@ -8,9 +8,10 @@ Requirements Platform-Specific Setup ----------------------- -- [Linux (Ubuntu)](ubuntu.md) +- [Linux (Ubuntu)](ubuntu-16.04.md) - [Windows (msys2)](msys2.md) - [Windows (Visual Studio)](msvc.md) +- [Windows (WSL)](wsl.md) - [macOS (homebrew)](osx-10.9.md) - Linux/macOS/WSL via [Nix](https://nixos.org/nix/): Call `nix-shell` in the project root. That's it. - There is also an [**experimental** setup based purely on Nix](nix.md) that works fundamentally differently from the @@ -54,7 +55,7 @@ below for details. Add `-jN` for an appropriate `N` to `make` for a parallel build. To install the build see [Dev setup using -elan](index.md#dev-setup-using-elan) below. +elan](../dev/index.md#dev-setup-using-elan). Useful CMake Configuration Settings @@ -72,185 +73,7 @@ Pass these along with the `cmake ../..` command. see also `.github/workflows/ci.yml` for the CI config. Lean will automatically use [CCache](https://ccache.dev/) if available to avoid -redundant builds, especially after stage 0 has been updated (see below). - -Lean Build Pipeline -------------------- - -Since version 4, Lean is a partially bootstrapped program: most parts of the -frontend and compiler are written in Lean itself and thus need to be built before -building Lean itself - which is needed to again build those parts. This cycle is -broken by using pre-built C files checked into the repository (which ultimately -go back to a point where the Lean compiler was not written in Lean) in place of -these Lean inputs and then compiling everything in multiple stages up to a fixed -point. The build directory is organized in these stages: - -```bash -stage0/ - # Bootstrap binary built from stage0/src/. - # We do not use any other files from this directory in further stages. - bin/lean -stage1/ - include/ - config.h # config variables used to build `lean` such as use allocator - runtime/lean.h # runtime headers, used by extracted C code, uses `config.h` - share/lean/ - Makefile # used by `leanmake` - lib/ - lean/**/*.olean # the Lean library (incl. the compiler) compiled by the previous stage's `lean` - temp/**/*.{c,o} # the library extracted to C and compiled by `leanc` - libInit.a libStd.a libLean.a # static libraries of the Lean library - libleancpp.a # a static library of the C++ sources of Lean - bin/ - lean # the Lean compiler & server linked together from the above libraries - leanc # a wrapper around a C compiler supplying search paths etc - leanmake # a wrapper around `make` supplying the Makefile above -stage2/... -stage3/... -``` - -Stage 0 can be viewed as a blackbox since it does not depend on any local -changes and is equivalent to downloading a bootstrapping binary as done in other -compilers. The build for any other stage starts by building the runtime and -standard library from `src/`, using the `lean` binary from the previous stage in -the latter case, which are then assembled into a new `bin/lean` binary. - -Each stage can be built by calling `make stageN` in the root build folder. -Running just `make` will default to stage 1, which is usually sufficient for -testing changes on the test suite or other files outside of the stdlib. However, -it might happen that the stage 1 compiler is not able to load its own stdlib, -e.g. when changing the .olean format: the stage 1 stdlib will use the format -generated by the stage 0 compiler, but the stage 1 compiler will expect the new -format. In this case, we should continue with building and testing stage 2 -instead, which will both build and expect the new format. Note that this is only -possible because when building a stage's stdlib, we use the previous compiler -but never load the previous stdlib (since everything is `prelude`). We can also -use stage 2 to test changes in the compiler or other "meta" parts, i.e. changes -that affect the produced (.olean or .c) code, on the stdlib and compiler itself. -We are not aware of any "meta-meta" parts that influence more than two stages of -compilation, so stage 3 should always be identical to stage 2 and only exists as -a sanity check. - -In summary, doing a standard build via `make` involves these steps: - -1. compile the `stage0/src` archived sources into `stage0/bin/lean` -1. use it to compile the current library (*including* your changes) into `stage1/lib` -1. link that and the current C++ code from `src/` into `stage1/bin/lean` - -You now have a Lean binary and library that include your changes, though their -own compilation was not influenced by them, that you can use to test your -changes on test programs whose compilation *will* be influenced by the changes. - -Finally, when we want to use new language features in the library, we need to -update the stage 0 compiler, which can be done via `make -C stageN update-stage0`. -`make update-stage0` without `-C` defaults to stage1. - -### Further Bootstrapping Complications - -As written above, changes in meta code in the current stage usually will only -affect later stages. This is an issue in two specific cases. - -* For *non-builtin* meta code such as `notation`s or `macro`s in - `Notation.lean`, we expect changes to affect the current file and all later - files of the same stage immediately, just like outside the stdlib. To ensure - this, we need to build the stage using `-Dinterpreter.prefer_native=false` - - otherwise, when executing a macro, the interpreter would notice that there is - already a native symbol available for this function and run it instead of the - new IR, but the symbol is from the previous stage! - - To make matters more complicated, while `false` is a reasonable default - incurring only minor overhead (`ParserDescr`s and simple macros are cheap to - interpret), there are situations where we *need* to set the option to `true`: - when the interpreter is executed from the native code of the previous stage, - the type of the value it computes must be identical to/ABI-compatible with the - type in the previous stage. For example, if we add a new parameter to `Macro` - or reorder constructors in `ParserDescr`, building the stage with the - interpreter will likely fail. Thus we need to set `interpreter.prefer_native` - to `true` in such cases to "freeze" meta code at their versions in the - previous stage; no new meta code should be introduced in this stage. Any - further stages (e.g. after an `update-stage0`) will then need to be compiled - with the flag set to `false` again since they will expect the new signature. - - For an example, see https://github.com/leanprover/lean4/commit/da4c46370d85add64ef7ca5e7cc4638b62823fbb. - -* For the special case of *quotations*, it is desirable to have changes in - built-in parsers affect them immediately: when the changes in the parser - become active in the next stage, macros implemented via quotations should - generate syntax trees compatible with the new parser, and quotation patterns - in macro and elaborators should be able to match syntax created by the new - parser and macros. Since quotations capture the syntax tree structure during - execution of the current stage and turn it into code for the next stage, we - need to run the current stage's built-in parsers in quotation via the - interpreter for this to work. Caveats: - * Since interpreting full parsers is not nearly as cheap and we rarely change - built-in syntax, this needs to be opted in using `-Dinternal.parseQuotWithCurrentStage=true`. - * The parser needs to be reachable via an `import` statement, otherwise the - version of the previous stage will silently be used. - * Only the parser code (`Parser.fn`) is affected; all metadata such as leading - tokens is taken from the previous stage. - - For an example, see https://github.com/leanprover/lean4/commit/f9dcbbddc48ccab22c7674ba20c5f409823b4cc1#diff-371387aed38bb02bf7761084fd9460e4168ae16d1ffe5de041b47d3ad2d22422 - (from before the flag defaulted to `false`). - -To modify either of these flags both for building and editing the stdlib, adjust -the code in `stage0/src/stdlib_flags.h`. The flags will automatically be reset -on the next `update-stage0` when the file is overwritten with the original -version in `src/`. - -Development Setup ------------------ - -After building a stage, you can invoke `make -C stageN test` (or, even better, -`make -C stageN test ARGS=-jN` to make `ctest` parallel) to run the Lean test suite. -`make test` without `-C` defaults to stage1. While the Lean tests will -automatically use that stage's corresponding Lean executables, for running tests -or compiling Lean programs manually, you need to put them into your `PATH` -yourself. A simple option for doing that is to use -[`elan`](https://github.com/leanprover/elan), see the next section. - -You can use any of the [supported editors](../setup.md) for editing the Lean source -code. If you set up `elan` as below, opening `src/` as a *workspace folder* should -ensure that stage 0 will be used for file in that directory. You should also set the -`LEAN_SRC_PATH` environment variable to the path of the `src/` directory to enable -go-to-definition in the stdlib (automatically set when using `nix-shell`). - -Dev setup using elan --------------------- - -You can use [`elan`](https://github.com/leanprover/elan) to easily switch between -stages and build configurations based on the current directory, both for the -`lean/leanc/leanmake` binaries in your shell's PATH and inside your editor. - -If you haven't already installed elan, you can do so, without installing a -default version of Lean, using -```bash -curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -``` -You can use `elan toolchain link` to give a specific stage build directory a -reference name, then use `elan override set` to associate such a name to the -current directory. We usually want to use `stage0` for editing files in `src` -and `stage1` for everything else (e.g. tests). -``` -# in the Lean rootdir -elan toolchain link lean4 build/release/stage1 -elan toolchain link lean4-stage0 build/release/stage0 -# make `lean` etc. point to stage1 in the rootdir and subdirs -elan override set lean4 -cd src -# make `lean` etc. point to stage0 anywhere inside `src` -elan override set lean4-stage0 -``` -You can also use the `+toolchain` shorthand (e.g. `lean +lean4-debug`) to switch -toolchains on the spot. `lean4-mode` will automatically use the `lean` executable -associated with the directory of the current file as long as `lean4-rootdir` is -unset and `~/.elan/bin` is in your `exec-path`. Where Emacs sources the -`exec-path` from can be a bit unclear depending on your configuration, so -alternatively you can also set `lean4-rootdir` to `"~/.elan"` explicitly. - -You might find that debugging through elan, e.g. via `gdb lean`, disables some -things like symbol autocompletion because at first only the elan proxy binary -is loaded. You can instead pass the explicit path to `bin/lean` in your build -folder to gdb, or use `gdb $(elan which lean)`. +redundant builds, especially after stage 0 has been updated. Troubleshooting --------------- diff --git a/doc/make/msvc.md b/doc/make/msvc.md index 6e585e9c5a..0fcc87c8d6 100644 --- a/doc/make/msvc.md +++ b/doc/make/msvc.md @@ -1,10 +1,10 @@ -Compiling Lean with Visual Studio ---------------------------------- +# Compiling Lean with Visual Studio WARNING: Compiling Lean with Visual Studio doesn't currently work. There's an ongoing effort to port Lean to Visual Studio. The instructions below are for VS 2017. +In the meantime you can use [MSYS2](msys2.md) or [WSL](wsl.md). ## Installing dependencies @@ -20,15 +20,14 @@ In each of the targets, add the following snippet (i.e., after every `ctestCommandArgs`): ```json - "variables": [ - { - "name": "CMAKE_TOOLCHAIN_FILE", - "value": "C:\\path\\to\\vcpkg\\scripts\\buildsystems\\vcpkg.cmake" - } - ] + "variables": [ + { + "name": "CMAKE_TOOLCHAIN_FILE", + "value": "C:\\path\\to\\vcpkg\\scripts\\buildsystems\\vcpkg.cmake" + } + ] ``` - ## Enable Intellisense In Visual Studio, press Ctrl+Q and type `CppProperties.json` and press Enter. diff --git a/doc/make/msys2.md b/doc/make/msys2.md index cf3d493c02..b917986205 100644 --- a/doc/make/msys2.md +++ b/doc/make/msys2.md @@ -1,13 +1,13 @@ [msys2]: http://msys2.github.io [pacman]: https://wiki.archlinux.org/index.php/pacman -Lean for Windows ----------------- +# Lean for Windows A native Lean binary for Windows can be generated using [MSYS2][msys2]. It is easy to install all dependencies, it produces native 64/32-binaries, and supports a C++14 compiler. +An alternative to MSYS2 is to use [Lean in Windows WSL](wsl.md). ## Installing dependencies @@ -26,19 +26,22 @@ pacman -S make python mingw-w64-x86_64-cmake mingw-w64-x86_64-clang mingw-w64-x8 You should now be able to run these commands: ```bash -gcc --version +clang --version cmake --version ``` Then follow the [generic build instructions](index.md) in the MSYS2 -MinGW shell, using `cmake ../.. -G "Unix Makefiles"` instead of `cmake -../..`. This ensures that cmake will call `sh` instead of `cmd.exe` -for script tasks. +MinGW shell, using: +``` +cmake ../.. -G "Unix Makefiles" -DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ +``` +instead of `cmake ../..`. This ensures that cmake will call `sh` instead of `cmd.exe` +for script tasks and it will use the clang compiler instead of gcc, which is required. ## Install lean Follow the steps in [Dev setup using -elan](index.md#dev-setup-using-elan) regarding installation of the +elan](../dev/index.md#dev-setup-using-elan) regarding installation of the bits you just built. Note that in an msys2 environment `elan-init.sh` reports you need to add `%USERPROFILE%\.elan\bin` to your path, but of course in msys2 that needs to be a valid linux style path, like this: diff --git a/doc/make/nix.md b/doc/make/nix.md index 5e3b43583c..002afb7f83 100644 --- a/doc/make/nix.md +++ b/doc/make/nix.md @@ -1,6 +1,8 @@ +# Building with Nix + While [Nix](https://nixos.org/nix/) can be used to quickly open a shell with all dependencies for the [standard setup](index.md) installed, the user-facing [Nix Setup](../setup.md#nix-setup) can also be used to work *on* Lean. -# Setup +## Setup Follow the setup in the link above; to open the Lean shell inside a Lean checkout, you can also use ```bash @@ -20,7 +22,7 @@ sudo mkdir -m0770 -p /nix/var/cache/ccache nix shell .#nixpkgs.coreutils -c sudo chown --reference=/nix/store /nix/var/cache/ccache ``` -# Basic Build Commands +## Basic Build Commands From the Lean root directory inside the Lean shell: ```bash @@ -36,7 +38,7 @@ nix build . # build stage 1 nix build # dito ``` -# Build Process Description +## Build Process Description The Nix build process conceptually works the same as described in [Lean Build Pipeline](index.md#lean-build-pipeline). However, there are two important differences in practice apart from the standard Nix properties (hermeneutic, reproducible builds stored in a global hash-indexed store etc.): @@ -45,7 +47,7 @@ This is actually a general property of Nix flakes, and has the benefit of making * Only files reachable from `src/Lean.lean` are compiled. This is because modules are discovered not from a directory listing anymore but by recursively compiling all dependencies of that top module. -# Editor Integration +## Editor Integration As in the standard Nix setup. After adding `src/` as an LSP workspace, it should automatically fall back to using stage 0 in there. @@ -55,7 +57,7 @@ there is no mutable directory incrementally filled by the build that we could po Instead, `emacs-dev` will gather the individual dependency outputs from the Nix store when checking a file -- and build them on the fly when necessary. However, it will only ever load changes saved to disk, not ones opened in other buffers. -# Other Fun Stuff to Do with Nix +## Other Fun Stuff to Do with Nix Open Emacs with Lean set up from an arbitrary commit (without even cloning Lean beforehand... if your Nix is new enough): ```bash @@ -90,7 +92,7 @@ This setup will inadvertently change your `flake.lock` file, which you can rever ...more surely to come... -# Debugging +## Debugging Since Nix copies all source files before compilation, you will need to map debug symbols back to the original path using `set substitute-path` in GDB. For example, for a build on Linux with the Nix sandbox activated: diff --git a/doc/make/osx-10.9.md b/doc/make/osx-10.9.md index 68c7122bdb..301fe55fd9 100644 --- a/doc/make/osx-10.9.md +++ b/doc/make/osx-10.9.md @@ -1,11 +1,10 @@ -Install Packages on OS X 10.9 ------------------------------ +# Install Packages on OS X 10.9 + We assume that you are using [homebrew][homebrew] as a package manager. [homebrew]: http://brew.sh -Compilers ---------- +## Compilers You need a C++11-compatible compiler to build Lean. As of November 2014, you have three options: @@ -18,29 +17,30 @@ We recommend to use Apple's clang++ because it is pre-shipped with OS X and requires no further installation. To install gcc-4.9.1 via homebrew, please execute: - - brew install gcc - +```bash +brew install gcc +``` To install clang++-3.5 via homebrew, please execute: - - brew install llvm --with-clang --with-asan - +```bash +brew install llvm --with-clang --with-asan +``` To use compilers other than the default one (Apple's clang++), you need to use `-DCMAKE_CXX_COMPILER` option to specify the compiler that you want to use when you run `cmake`. For example, do the following to use `g++`. +```bash +cmake -DCMAKE_CXX_COMPILER=g++ ... +``` - cmake -DCMAKE_CXX_COMPILER=g++ ... +## Required Packages: CMake, GMP +```bash +brew install cmake +brew install gmp +``` -Required Packages: CMake, GMP ---------------------- +## Recommended Packages: CCache - brew install cmake - brew install gmp - - -Recommended Packages: CCache ----------------------------- - - brew install ccache +```bash +brew install ccache +``` \ No newline at end of file diff --git a/doc/make/ubuntu-16.04.md b/doc/make/ubuntu-16.04.md index 6b7c7df681..089e910927 100644 --- a/doc/make/ubuntu-16.04.md +++ b/doc/make/ubuntu-16.04.md @@ -1,8 +1,12 @@ -Installing Lean on Ubuntu 16.04 -------------------------------- +# Installing Lean on Ubuntu 16.04 -### Basic packages +## Build Dependencies + +Please ensure you have the following build tools available and then +follow the [generic build instructions](index.md). + +## Basic packages ```bash -sudo apt-get install git libgmp-dev cmake ccache +sudo apt-get install git libgmp-dev cmake ccache gcc-10 g++-10 ``` diff --git a/doc/make/wsl.md b/doc/make/wsl.md new file mode 100644 index 0000000000..894140a1a8 --- /dev/null +++ b/doc/make/wsl.md @@ -0,0 +1,56 @@ +[vscode]: https://code.visualstudio.com/Download +[wsl]: https://docs.microsoft.com/en-us/windows/wsl/install-win10 + +# Lean in Windows WSL + +As an alternative to the [MSYS2](msys2.md) setup you can also use the +[Windows Subsystem for Linux][wsl] to build Lean there, but edit and +debug using [Visual Studio Code][vscode] in Windows. + +For the most part setup in WSL is the same as +[Ubuntu](Ubuntu-16.04.md). This document provides additional +information on how to setup Windows Visual Studio Code remote +debugging into your WSL environment using the lean extension running +in WSL. + +It is recommended that you setup Ubuntu in [WSL +2](https://docs.microsoft.com/en-us/windows/wsl/compare-versions). +Then follow the [Dev setup using elan](../dev/index.md#dev-setup-using-elan). + +## Visual Studio Code setup on Windows + +Install [Visual Studio Code][vscode] on Windows. Install the VS Code +`Remote Development` extension from Microsoft. This extension +includes the `Remote - WSL` extension. Install the lean4 extension but +into the WSL using: `Install in WSL: Ubuntu` + +Type `Ctrl+Shift+P` and select `Remote-WSL: Open Folder in WSL...` to +open a folder containing your hello world lean package. + +When everything is working you should see this: + +![screenshot](../images/code-wsl.png) + +with a functioning infoview, syntax coloring and tooltips. + +## Troubleshooting + +**Connection to server is erroring. Shutting down server.** + +If your `leanpkg` has a `build` folder try deleting it. Lean .olean +binaries are not cross platform so if the binaries were copied from a +different platform they need to be deleted so that the new build is +created for your platform. + +**Logs are showing up with a windows file path** + +Check that you have not set a windows path in your +`lean4.serverLogging.path` Visual Studio Code setting. it is best if +this setting is set as follows: + +```json + "lean4.serverLogging.path": "logs" +``` + +This will result in a logs folder being created inside your lean +package folder in the WSL file system. \ No newline at end of file diff --git a/doc/make/wsl2.md b/doc/make/wsl2.md new file mode 100644 index 0000000000..f86b60582c --- /dev/null +++ b/doc/make/wsl2.md @@ -0,0 +1 @@ +# Windows with WSL