From b78523ff2c3349e98686871891028069edfa7523 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Apr 2018 11:08:59 +0200 Subject: move etc/ files to the root and remove obsolete ones --- AUTHORS | 15 ++ CeCILL-B | 514 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ ChangeLog | 141 ++++++++++++++++ etc/AUTHORS | 15 -- etc/CeCILL-B | 514 --------------------------------------------------------- etc/ChangeLog | 141 ---------------- etc/INSTALL.md | 78 --------- etc/Makefile | 6 - etc/README | 40 ----- 9 files changed, 670 insertions(+), 794 deletions(-) create mode 100644 AUTHORS create mode 100644 CeCILL-B create mode 100644 ChangeLog delete mode 100644 etc/AUTHORS delete mode 100644 etc/CeCILL-B delete mode 100644 etc/ChangeLog delete mode 100644 etc/INSTALL.md delete mode 100644 etc/Makefile delete mode 100644 etc/README diff --git a/AUTHORS b/AUTHORS new file mode 100644 index 0000000..848f504 --- /dev/null +++ b/AUTHORS @@ -0,0 +1,15 @@ +Andrea Asperti University of Bologna - Microsoft Inria Joint Centre +Jeremy Avigad Carnegie Mellon University - Microsoft Inria Joint Centre +Yves Bertot Inria Sophia Antipolis - Microsoft Inria Joint Centre +Cyril Cohen LIX École Polytechnique - Microsoft Inria Joint Centre +François Garillot Microsoft Inria Joint Centre +Georges Gonthier Microsoft Research Cambridge - Microsoft Inria Joint Centre +Stéphane Le Roux Microsoft Inria Joint Centre +Assia Mahboubi Inria Saclay - Microsoft Inria Joint Centre +Sidi Ould Biha Inria Sophia Antipolis - Microsoft Inria Joint Centre +Ioana Pasca Inria Sophia Antipolis - Microsoft Inria Joint Centre +Laurence Rideau Inria Sophia Antipolis - Microsoft Inria Joint Centre +Alexey Solovyev University of Pittsburgh +Enrico Tassi Inria Saclay - Microsoft Inria Joint Centre +Laurent Théry Inria Sophia Antipolis - Microsoft Inria Joint Centre +Russell O'Connor Mc Master University - Microsoft Inria Joint Centre diff --git a/CeCILL-B b/CeCILL-B new file mode 100644 index 0000000..fe29f5c --- /dev/null +++ b/CeCILL-B @@ -0,0 +1,514 @@ +CeCILL-B FREE SOFTWARE LICENSE AGREEMENT + + + Notice + +This Agreement is a Free Software license agreement that is the result +of discussions between its authors in order to ensure compliance with +the two main principles guiding its drafting: + + * firstly, compliance with the principles governing the distribution + of Free Software: access to source code, broad rights granted to + users, + * secondly, the election of a governing law, French law, with which + it is conformant, both as regards the law of torts and + intellectual property law, and the protection that it offers to + both authors and holders of the economic rights over software. + +The authors of the CeCILL-B (for Ce[a] C[nrs] I[nria] L[ogiciel] L[ibre]) +license are: + +Commissariat à l'Energie Atomique - CEA, a public scientific, technical +and industrial research establishment, having its principal place of +business at 25 rue Leblanc, immeuble Le Ponant D, 75015 Paris, France. + +Centre National de la Recherche Scientifique - CNRS, a public scientific +and technological establishment, having its principal place of business +at 3 rue Michel-Ange, 75794 Paris cedex 16, France. + +Institut National de Recherche en Informatique et en Automatique - +INRIA, a public scientific and technological establishment, having its +principal place of business at Domaine de Voluceau, Rocquencourt, BP +105, 78153 Le Chesnay cedex, France. + + + Preamble + +This Agreement is an open source software license intended to give users +significant freedom to modify and redistribute the software licensed +hereunder. + +The exercising of this freedom is conditional upon a strong obligation +of giving credits for everybody that distributes a software +incorporating a software ruled by the current license so as all +contributions to be properly identified and acknowledged. + +In consideration of access to the source code and the rights to copy, +modify and redistribute granted by the license, users are provided only +with a limited warranty and the software's author, the holder of the +economic rights, and the successive licensors only have limited liability. + +In this respect, the risks associated with loading, using, modifying +and/or developing or reproducing the software by the user are brought to +the user's attention, given its Free Software status, which may make it +complicated to use, with the result that its use is reserved for +developers and experienced professionals having in-depth computer +knowledge. Users are therefore encouraged to load and test the +suitability of the software as regards their requirements in conditions +enabling the security of their systems and/or data to be ensured and, +more generally, to use and operate it in the same conditions of +security. This Agreement may be freely reproduced and published, +provided it is not altered, and that no provisions are either added or +removed herefrom. + +This Agreement may apply to any or all software for which the holder of +the economic rights decides to submit the use thereof to its provisions. + + + Article 1 - DEFINITIONS + +For the purpose of this Agreement, when the following expressions +commence with a capital letter, they shall have the following meaning: + +Agreement: means this license agreement, and its possible subsequent +versions and annexes. + +Software: means the software in its Object Code and/or Source Code form +and, where applicable, its documentation, "as is" when the Licensee +accepts the Agreement. + +Initial Software: means the Software in its Source Code and possibly its +Object Code form and, where applicable, its documentation, "as is" when +it is first distributed under the terms and conditions of the Agreement. + +Modified Software: means the Software modified by at least one +Contribution. + +Source Code: means all the Software's instructions and program lines to +which access is required so as to modify the Software. + +Object Code: means the binary files originating from the compilation of +the Source Code. + +Holder: means the holder(s) of the economic rights over the Initial +Software. + +Licensee: means the Software user(s) having accepted the Agreement. + +Contributor: means a Licensee having made at least one Contribution. + +Licensor: means the Holder, or any other individual or legal entity, who +distributes the Software under the Agreement. + +Contribution: means any or all modifications, corrections, translations, +adaptations and/or new functions integrated into the Software by any or +all Contributors, as well as any or all Internal Modules. + +Module: means a set of sources files including their documentation that +enables supplementary functions or services in addition to those offered +by the Software. + +External Module: means any or all Modules, not derived from the +Software, so that this Module and the Software run in separate address +spaces, with one calling the other when they are run. + +Internal Module: means any or all Module, connected to the Software so +that they both execute in the same address space. + +Parties: mean both the Licensee and the Licensor. + +These expressions may be used both in singular and plural form. + + + Article 2 - PURPOSE + +The purpose of the Agreement is the grant by the Licensor to the +Licensee of a non-exclusive, transferable and worldwide license for the +Software as set forth in Article 5 hereinafter for the whole term of the +protection granted by the rights over said Software. + + + Article 3 - ACCEPTANCE + +3.1 The Licensee shall be deemed as having accepted the terms and +conditions of this Agreement upon the occurrence of the first of the +following events: + + * (i) loading the Software by any or all means, notably, by + downloading from a remote server, or by loading from a physical + medium; + * (ii) the first time the Licensee exercises any of the rights + granted hereunder. + +3.2 One copy of the Agreement, containing a notice relating to the +characteristics of the Software, to the limited warranty, and to the +fact that its use is restricted to experienced users has been provided +to the Licensee prior to its acceptance as set forth in Article 3.1 +hereinabove, and the Licensee hereby acknowledges that it has read and +understood it. + + + Article 4 - EFFECTIVE DATE AND TERM + + + 4.1 EFFECTIVE DATE + +The Agreement shall become effective on the date when it is accepted by +the Licensee as set forth in Article 3.1. + + + 4.2 TERM + +The Agreement shall remain in force for the entire legal term of +protection of the economic rights over the Software. + + + Article 5 - SCOPE OF RIGHTS GRANTED + +The Licensor hereby grants to the Licensee, who accepts, the following +rights over the Software for any or all use, and for the term of the +Agreement, on the basis of the terms and conditions set forth hereinafter. + +Besides, if the Licensor owns or comes to own one or more patents +protecting all or part of the functions of the Software or of its +components, the Licensor undertakes not to enforce the rights granted by +these patents against successive Licensees using, exploiting or +modifying the Software. If these patents are transferred, the Licensor +undertakes to have the transferees subscribe to the obligations set +forth in this paragraph. + + + 5.1 RIGHT OF USE + +The Licensee is authorized to use the Software, without any limitation +as to its fields of application, with it being hereinafter specified +that this comprises: + + 1. permanent or temporary reproduction of all or part of the Software + by any or all means and in any or all form. + + 2. loading, displaying, running, or storing the Software on any or + all medium. + + 3. entitlement to observe, study or test its operation so as to + determine the ideas and principles behind any or all constituent + elements of said Software. This shall apply when the Licensee + carries out any or all loading, displaying, running, transmission + or storage operation as regards the Software, that it is entitled + to carry out hereunder. + + + 5.2 ENTITLEMENT TO MAKE CONTRIBUTIONS + +The right to make Contributions includes the right to translate, adapt, +arrange, or make any or all modifications to the Software, and the right +to reproduce the resulting software. + +The Licensee is authorized to make any or all Contributions to the +Software provided that it includes an explicit notice that it is the +author of said Contribution and indicates the date of the creation thereof. + + + 5.3 RIGHT OF DISTRIBUTION + +In particular, the right of distribution includes the right to publish, +transmit and communicate the Software to the general public on any or +all medium, and by any or all means, and the right to market, either in +consideration of a fee, or free of charge, one or more copies of the +Software by any means. + +The Licensee is further authorized to distribute copies of the modified +or unmodified Software to third parties according to the terms and +conditions set forth hereinafter. + + + 5.3.1 DISTRIBUTION OF SOFTWARE WITHOUT MODIFICATION + +The Licensee is authorized to distribute true copies of the Software in +Source Code or Object Code form, provided that said distribution +complies with all the provisions of the Agreement and is accompanied by: + + 1. a copy of the Agreement, + + 2. a notice relating to the limitation of both the Licensor's + warranty and liability as set forth in Articles 8 and 9, + +and that, in the event that only the Object Code of the Software is +redistributed, the Licensee allows effective access to the full Source +Code of the Software at a minimum during the entire period of its +distribution of the Software, it being understood that the additional +cost of acquiring the Source Code shall not exceed the cost of +transferring the data. + + + 5.3.2 DISTRIBUTION OF MODIFIED SOFTWARE + +If the Licensee makes any Contribution to the Software, the resulting +Modified Software may be distributed under a license agreement other +than this Agreement subject to compliance with the provisions of Article +5.3.4. + + + 5.3.3 DISTRIBUTION OF EXTERNAL MODULES + +When the Licensee has developed an External Module, the terms and +conditions of this Agreement do not apply to said External Module, that +may be distributed under a separate license agreement. + + + 5.3.4 CREDITS + +Any Licensee who may distribute a Modified Software hereby expressly +agrees to: + + 1. indicate in the related documentation that it is based on the + Software licensed hereunder, and reproduce the intellectual + property notice for the Software, + + 2. ensure that written indications of the Software intended use, + intellectual property notice and license hereunder are included in + easily accessible format from the Modified Software interface, + + 3. mention, on a freely accessible website describing the Modified + Software, at least throughout the distribution term thereof, that + it is based on the Software licensed hereunder, and reproduce the + Software intellectual property notice, + + 4. where it is distributed to a third party that may distribute a + Modified Software without having to make its source code + available, make its best efforts to ensure that said third party + agrees to comply with the obligations set forth in this Article . + +If the Software, whether or not modified, is distributed with an +External Module designed for use in connection with the Software, the +Licensee shall submit said External Module to the foregoing obligations. + + + 5.3.5 COMPATIBILITY WITH THE CeCILL AND CeCILL-C LICENSES + +Where a Modified Software contains a Contribution subject to the CeCILL +license, the provisions set forth in Article 5.3.4 shall be optional. + +A Modified Software may be distributed under the CeCILL-C license. In +such a case the provisions set forth in Article 5.3.4 shall be optional. + + + Article 6 - INTELLECTUAL PROPERTY + + + 6.1 OVER THE INITIAL SOFTWARE + +The Holder owns the economic rights over the Initial Software. Any or +all use of the Initial Software is subject to compliance with the terms +and conditions under which the Holder has elected to distribute its work +and no one shall be entitled to modify the terms and conditions for the +distribution of said Initial Software. + +The Holder undertakes that the Initial Software will remain ruled at +least by this Agreement, for the duration set forth in Article 4.2. + + + 6.2 OVER THE CONTRIBUTIONS + +The Licensee who develops a Contribution is the owner of the +intellectual property rights over this Contribution as defined by +applicable law. + + + 6.3 OVER THE EXTERNAL MODULES + +The Licensee who develops an External Module is the owner of the +intellectual property rights over this External Module as defined by +applicable law and is free to choose the type of agreement that shall +govern its distribution. + + + 6.4 JOINT PROVISIONS + +The Licensee expressly undertakes: + + 1. not to remove, or modify, in any manner, the intellectual property + notices attached to the Software; + + 2. to reproduce said notices, in an identical manner, in the copies + of the Software modified or not. + +The Licensee undertakes not to directly or indirectly infringe the +intellectual property rights of the Holder and/or Contributors on the +Software and to take, where applicable, vis-à-vis its staff, any and all +measures required to ensure respect of said intellectual property rights +of the Holder and/or Contributors. + + + Article 7 - RELATED SERVICES + +7.1 Under no circumstances shall the Agreement oblige the Licensor to +provide technical assistance or maintenance services for the Software. + +However, the Licensor is entitled to offer this type of services. The +terms and conditions of such technical assistance, and/or such +maintenance, shall be set forth in a separate instrument. Only the +Licensor offering said maintenance and/or technical assistance services +shall incur liability therefor. + +7.2 Similarly, any Licensor is entitled to offer to its licensees, under +its sole responsibility, a warranty, that shall only be binding upon +itself, for the redistribution of the Software and/or the Modified +Software, under terms and conditions that it is free to decide. Said +warranty, and the financial terms and conditions of its application, +shall be subject of a separate instrument executed between the Licensor +and the Licensee. + + + Article 8 - LIABILITY + +8.1 Subject to the provisions of Article 8.2, the Licensee shall be +entitled to claim compensation for any direct loss it may have suffered +from the Software as a result of a fault on the part of the relevant +Licensor, subject to providing evidence thereof. + +8.2 The Licensor's liability is limited to the commitments made under +this Agreement and shall not be incurred as a result of in particular: +(i) loss due the Licensee's total or partial failure to fulfill its +obligations, (ii) direct or consequential loss that is suffered by the +Licensee due to the use or performance of the Software, and (iii) more +generally, any consequential loss. In particular the Parties expressly +agree that any or all pecuniary or business loss (i.e. loss of data, +loss of profits, operating loss, loss of customers or orders, +opportunity cost, any disturbance to business activities) or any or all +legal proceedings instituted against the Licensee by a third party, +shall constitute consequential loss and shall not provide entitlement to +any or all compensation from the Licensor. + + + Article 9 - WARRANTY + +9.1 The Licensee acknowledges that the scientific and technical +state-of-the-art when the Software was distributed did not enable all +possible uses to be tested and verified, nor for the presence of +possible defects to be detected. In this respect, the Licensee's +attention has been drawn to the risks associated with loading, using, +modifying and/or developing and reproducing the Software which are +reserved for experienced users. + +The Licensee shall be responsible for verifying, by any or all means, +the suitability of the product for its requirements, its good working +order, and for ensuring that it shall not cause damage to either persons +or properties. + +9.2 The Licensor hereby represents, in good faith, that it is entitled +to grant all the rights over the Software (including in particular the +rights set forth in Article 5). + +9.3 The Licensee acknowledges that the Software is supplied "as is" by +the Licensor without any other express or tacit warranty, other than +that provided for in Article 9.2 and, in particular, without any warranty +as to its commercial value, its secured, safe, innovative or relevant +nature. + +Specifically, the Licensor does not warrant that the Software is free +from any error, that it will operate without interruption, that it will +be compatible with the Licensee's own equipment and software +configuration, nor that it will meet the Licensee's requirements. + +9.4 The Licensor does not either expressly or tacitly warrant that the +Software does not infringe any third party intellectual property right +relating to a patent, software or any other property right. Therefore, +the Licensor disclaims any and all liability towards the Licensee +arising out of any or all proceedings for infringement that may be +instituted in respect of the use, modification and redistribution of the +Software. Nevertheless, should such proceedings be instituted against +the Licensee, the Licensor shall provide it with technical and legal +assistance for its defense. Such technical and legal assistance shall be +decided on a case-by-case basis between the relevant Licensor and the +Licensee pursuant to a memorandum of understanding. The Licensor +disclaims any and all liability as regards the Licensee's use of the +name of the Software. No warranty is given as regards the existence of +prior rights over the name of the Software or as regards the existence +of a trademark. + + + Article 10 - TERMINATION + +10.1 In the event of a breach by the Licensee of its obligations +hereunder, the Licensor may automatically terminate this Agreement +thirty (30) days after notice has been sent to the Licensee and has +remained ineffective. + +10.2 A Licensee whose Agreement is terminated shall no longer be +authorized to use, modify or distribute the Software. However, any +licenses that it may have granted prior to termination of the Agreement +shall remain valid subject to their having been granted in compliance +with the terms and conditions hereof. + + + Article 11 - MISCELLANEOUS + + + 11.1 EXCUSABLE EVENTS + +Neither Party shall be liable for any or all delay, or failure to +perform the Agreement, that may be attributable to an event of force +majeure, an act of God or an outside cause, such as defective +functioning or interruptions of the electricity or telecommunications +networks, network paralysis following a virus attack, intervention by +government authorities, natural disasters, water damage, earthquakes, +fire, explosions, strikes and labor unrest, war, etc. + +11.2 Any failure by either Party, on one or more occasions, to invoke +one or more of the provisions hereof, shall under no circumstances be +interpreted as being a waiver by the interested Party of its right to +invoke said provision(s) subsequently. + +11.3 The Agreement cancels and replaces any or all previous agreements, +whether written or oral, between the Parties and having the same +purpose, and constitutes the entirety of the agreement between said +Parties concerning said purpose. No supplement or modification to the +terms and conditions hereof shall be effective as between the Parties +unless it is made in writing and signed by their duly authorized +representatives. + +11.4 In the event that one or more of the provisions hereof were to +conflict with a current or future applicable act or legislative text, +said act or legislative text shall prevail, and the Parties shall make +the necessary amendments so as to comply with said act or legislative +text. All other provisions shall remain effective. Similarly, invalidity +of a provision of the Agreement, for any reason whatsoever, shall not +cause the Agreement as a whole to be invalid. + + + 11.5 LANGUAGE + +The Agreement is drafted in both French and English and both versions +are deemed authentic. + + + Article 12 - NEW VERSIONS OF THE AGREEMENT + +12.1 Any person is authorized to duplicate and distribute copies of this +Agreement. + +12.2 So as to ensure coherence, the wording of this Agreement is +protected and may only be modified by the authors of the License, who +reserve the right to periodically publish updates or new versions of the +Agreement, each with a separate number. These subsequent versions may +address new issues encountered by Free Software. + +12.3 Any Software distributed under a given version of the Agreement may +only be subsequently distributed under the same version of the Agreement +or a subsequent version. + + + Article 13 - GOVERNING LAW AND JURISDICTION + +13.1 The Agreement is governed by French law. The Parties agree to +endeavor to seek an amicable solution to any disagreements or disputes +that may arise during the performance of the Agreement. + +13.2 Failing an amicable solution within two (2) months as from their +occurrence, and unless emergency proceedings are necessary, the +disagreements or disputes shall be referred to the Paris Courts having +jurisdiction, by the more diligent Party. + + +Version 1.0 dated 2006-09-05. diff --git a/ChangeLog b/ChangeLog new file mode 100644 index 0000000..12d6ef4 --- /dev/null +++ b/ChangeLog @@ -0,0 +1,141 @@ +07/09/2016 - compatibility with Coq 8.7 and several small fixes - + version 1.6.2 and upcomming version 1.7 + * Compatibility with Coq 8.7 + * Lost compatibility with Coq 8.4 + +07/09/2016 - compatibility with Coq 8.7 and several small fixes - + upcomming version 1.7 + * New Theorems: + dec_factor_theorem, abstract_context, + mul_bin_down, mul_bin_left + + * Renamings or replacements: + mul_Sm_binm -> mul_bin_diag + divn1 -> divz1 (in intdiv) + + * Generalized or extended: + ltngtP, contra_eq, contra_neq, odd_opp + + * Plugin: + ssrpattern: compose nicely with Tactic Notation + +25/08/2016 - refactoring of algC and complex in ssrnum - + upcomming version 1.7 + * ssrnum's interface numClosedFieldType factors some theory from + both complex and algC. Because of that Re, Im, 'i, conjC, n.-root + and sqrtC are not specialized to algC anymore. In case of + ambiguity, they should be instanciated with algC using typing + constraints. Moreoever all the lemmas from ssrnum that used to + be in algC (like conjCK), now take an extra nonmaximal implicit + argument (C : numClosedFieldType) which could break some proofs. + Additionally, ad-hoc constructions from complex.v like -*+ or + complex.Re are now deprecated and one should rely solely on the + ssrnum interface. The next revision might definietly hide those + constructions under a module. + + * Structures that change: + numClosedFieldType + + * Renamed and generalized definitions: + rootC -> nthroot + algRe -> Re + algIm -> Im + algCi -> imaginaryC + + * Renamed and generalized theorems: + Every theorem from ssrnum that used to be in algC + +24/11/2015 - major reorganization of the archive - version 1.6 + * Files split into subdirectories: ssreflect, algebra, fingroup, + solvable, field and character. In this way the user can decide + to compile only the subset of the Mathematical Components library + that is relevant to her. Note that this introduces a possible + incompatibility for users of the previous version. A replacement + scheme is suggested in the installation notes. + + * The archive is now open and based on git. Public mirror at: + https://github.com/math-comp/math-comp + + * Sources of the reference manual of the Ssreflect tactic language are + also open and available at: + https://github.com/math-comp/ssr-manual + Pull requests improving the documentation are welcome. + + * Renamings or replacements: + conjC_closed -> cfConjC_closed + class_transr -> class_eqP + cfclass_transl -> cfclass_transr + nontrivial_ideal -> proper_ideal + zchar_orthonormalP -> vchar_orthonormalP + + * Definitions that changed: + seq_sub + + * Statements that changed: + orbit_in_transl, orbit_sym, orbit_trans, orbit_transl, orbit_transr, + cfAut_char, cfConjC_char, invg_lcosets, lcoset_transl, + lcoset_transr, rcoset_transl, rcoset_transr, mem2_last, + bind_unless, unless_contra, all_and2, all_and3, all_and4, all_and5, + ltr0_neq0, ltr_prod, Zisometry_of_iso + + * New definitions: + adhoc_seq_sub_choiceMixin, adhoc_seq_sub_[choice|fin]Type + + * New theorems: + orbit_in_eqP, cards_draws, cfAut_lin_char, cfConjC_lin_char, + extend_cfConjC_subset, isometry_of_free, cfAutK, cfAutVK, + lcoset_eqP, rcoset_eqP, class_eqP, gFsub_trans, gFnorms, + gFchar_trans, gFnormal_trans, gFnorm_trans, mem2_seq1, + dvdn_fact, prime_above, subKr, subrI, subIr, subr0_eq, + divrI, divIr, divKr, divfI, divIf, divKf, impliesP, impliesPn, + unlessL, unlessR, unless_sym, unlessP (coercion), classicW, + ltr_prod_nat + + * New notation: "\unless C, P" + +12/03/2014 - split the archive in SSReflect and MathComp - version 1.5 + * With this release "ssreflect" has been split into two packages. + The Ssreflect one contains the proof language (plugin for Coq) and a + small set of core theory libraries about boolean, natural numbers, + sequences, decidable equality and finite types. The Mathematical + Components one contains advanced theory files covering a wider + spectrum of mathematics. + + * With respect to version 1.4 the proof language got a few new + features related to forward reasoning and some bugfixes. The + Mathematical Components library features 16 new theory files and in + particular: some field and Galois theory, advanced character theory + and a construction of algebraic numbers. + +05/09/2012 - ssreflect - version 1.4 + * With this release the plugin code received many bug fixes and the + existing libraries relevant updates. This release also includes + some new libraries on the following topics: rational numbers, + divisibility of integers, F-algebras, finite dimensional field + extensions and Euclidean division for polynomials over a ring. + + * The release includes a major code refactoring of the plugin for Coq + 8.4. In particular a documented ML API to access the pattern matching + facilities of Ssreflect from third party plugins has been introduced. + +14/03/2011 - ssreflect - version 1.3 + * The tactic language has been extended with several new features, + inspired by the five years of intensive use in our project. However we + have kept the core of the language unchanged; the new library compiles + with Ssreflect 1.2. Users of a Coq 8.2 toplevel statically linked + with Ssreflect 1.2 need to comment the Declare ML Module "ssreflect" + line in ssreflect.v to properly compile the 1.3 library. We will + continue supporting new releases of Coq in due course. + + * The new library adds general linear algebra (matrix rank, subspaces) + and all of the advanced finite group that was developed in the course + of completing the Local Analysis part of the Odd Order Theorem, + starting from the Sylow and Hall theorems and including full structure + theorems for abelian, extremal and extraspecial groups, and general + (modular) linear representation theory. + +14/08/2009 - ssreflect - version 1.2 + * No change log + +18/03/2008 - ssreflect - version 1.1 + * First public release diff --git a/etc/AUTHORS b/etc/AUTHORS deleted file mode 100644 index 848f504..0000000 --- a/etc/AUTHORS +++ /dev/null @@ -1,15 +0,0 @@ -Andrea Asperti University of Bologna - Microsoft Inria Joint Centre -Jeremy Avigad Carnegie Mellon University - Microsoft Inria Joint Centre -Yves Bertot Inria Sophia Antipolis - Microsoft Inria Joint Centre -Cyril Cohen LIX École Polytechnique - Microsoft Inria Joint Centre -François Garillot Microsoft Inria Joint Centre -Georges Gonthier Microsoft Research Cambridge - Microsoft Inria Joint Centre -Stéphane Le Roux Microsoft Inria Joint Centre -Assia Mahboubi Inria Saclay - Microsoft Inria Joint Centre -Sidi Ould Biha Inria Sophia Antipolis - Microsoft Inria Joint Centre -Ioana Pasca Inria Sophia Antipolis - Microsoft Inria Joint Centre -Laurence Rideau Inria Sophia Antipolis - Microsoft Inria Joint Centre -Alexey Solovyev University of Pittsburgh -Enrico Tassi Inria Saclay - Microsoft Inria Joint Centre -Laurent Théry Inria Sophia Antipolis - Microsoft Inria Joint Centre -Russell O'Connor Mc Master University - Microsoft Inria Joint Centre diff --git a/etc/CeCILL-B b/etc/CeCILL-B deleted file mode 100644 index fe29f5c..0000000 --- a/etc/CeCILL-B +++ /dev/null @@ -1,514 +0,0 @@ -CeCILL-B FREE SOFTWARE LICENSE AGREEMENT - - - Notice - -This Agreement is a Free Software license agreement that is the result -of discussions between its authors in order to ensure compliance with -the two main principles guiding its drafting: - - * firstly, compliance with the principles governing the distribution - of Free Software: access to source code, broad rights granted to - users, - * secondly, the election of a governing law, French law, with which - it is conformant, both as regards the law of torts and - intellectual property law, and the protection that it offers to - both authors and holders of the economic rights over software. - -The authors of the CeCILL-B (for Ce[a] C[nrs] I[nria] L[ogiciel] L[ibre]) -license are: - -Commissariat à l'Energie Atomique - CEA, a public scientific, technical -and industrial research establishment, having its principal place of -business at 25 rue Leblanc, immeuble Le Ponant D, 75015 Paris, France. - -Centre National de la Recherche Scientifique - CNRS, a public scientific -and technological establishment, having its principal place of business -at 3 rue Michel-Ange, 75794 Paris cedex 16, France. - -Institut National de Recherche en Informatique et en Automatique - -INRIA, a public scientific and technological establishment, having its -principal place of business at Domaine de Voluceau, Rocquencourt, BP -105, 78153 Le Chesnay cedex, France. - - - Preamble - -This Agreement is an open source software license intended to give users -significant freedom to modify and redistribute the software licensed -hereunder. - -The exercising of this freedom is conditional upon a strong obligation -of giving credits for everybody that distributes a software -incorporating a software ruled by the current license so as all -contributions to be properly identified and acknowledged. - -In consideration of access to the source code and the rights to copy, -modify and redistribute granted by the license, users are provided only -with a limited warranty and the software's author, the holder of the -economic rights, and the successive licensors only have limited liability. - -In this respect, the risks associated with loading, using, modifying -and/or developing or reproducing the software by the user are brought to -the user's attention, given its Free Software status, which may make it -complicated to use, with the result that its use is reserved for -developers and experienced professionals having in-depth computer -knowledge. Users are therefore encouraged to load and test the -suitability of the software as regards their requirements in conditions -enabling the security of their systems and/or data to be ensured and, -more generally, to use and operate it in the same conditions of -security. This Agreement may be freely reproduced and published, -provided it is not altered, and that no provisions are either added or -removed herefrom. - -This Agreement may apply to any or all software for which the holder of -the economic rights decides to submit the use thereof to its provisions. - - - Article 1 - DEFINITIONS - -For the purpose of this Agreement, when the following expressions -commence with a capital letter, they shall have the following meaning: - -Agreement: means this license agreement, and its possible subsequent -versions and annexes. - -Software: means the software in its Object Code and/or Source Code form -and, where applicable, its documentation, "as is" when the Licensee -accepts the Agreement. - -Initial Software: means the Software in its Source Code and possibly its -Object Code form and, where applicable, its documentation, "as is" when -it is first distributed under the terms and conditions of the Agreement. - -Modified Software: means the Software modified by at least one -Contribution. - -Source Code: means all the Software's instructions and program lines to -which access is required so as to modify the Software. - -Object Code: means the binary files originating from the compilation of -the Source Code. - -Holder: means the holder(s) of the economic rights over the Initial -Software. - -Licensee: means the Software user(s) having accepted the Agreement. - -Contributor: means a Licensee having made at least one Contribution. - -Licensor: means the Holder, or any other individual or legal entity, who -distributes the Software under the Agreement. - -Contribution: means any or all modifications, corrections, translations, -adaptations and/or new functions integrated into the Software by any or -all Contributors, as well as any or all Internal Modules. - -Module: means a set of sources files including their documentation that -enables supplementary functions or services in addition to those offered -by the Software. - -External Module: means any or all Modules, not derived from the -Software, so that this Module and the Software run in separate address -spaces, with one calling the other when they are run. - -Internal Module: means any or all Module, connected to the Software so -that they both execute in the same address space. - -Parties: mean both the Licensee and the Licensor. - -These expressions may be used both in singular and plural form. - - - Article 2 - PURPOSE - -The purpose of the Agreement is the grant by the Licensor to the -Licensee of a non-exclusive, transferable and worldwide license for the -Software as set forth in Article 5 hereinafter for the whole term of the -protection granted by the rights over said Software. - - - Article 3 - ACCEPTANCE - -3.1 The Licensee shall be deemed as having accepted the terms and -conditions of this Agreement upon the occurrence of the first of the -following events: - - * (i) loading the Software by any or all means, notably, by - downloading from a remote server, or by loading from a physical - medium; - * (ii) the first time the Licensee exercises any of the rights - granted hereunder. - -3.2 One copy of the Agreement, containing a notice relating to the -characteristics of the Software, to the limited warranty, and to the -fact that its use is restricted to experienced users has been provided -to the Licensee prior to its acceptance as set forth in Article 3.1 -hereinabove, and the Licensee hereby acknowledges that it has read and -understood it. - - - Article 4 - EFFECTIVE DATE AND TERM - - - 4.1 EFFECTIVE DATE - -The Agreement shall become effective on the date when it is accepted by -the Licensee as set forth in Article 3.1. - - - 4.2 TERM - -The Agreement shall remain in force for the entire legal term of -protection of the economic rights over the Software. - - - Article 5 - SCOPE OF RIGHTS GRANTED - -The Licensor hereby grants to the Licensee, who accepts, the following -rights over the Software for any or all use, and for the term of the -Agreement, on the basis of the terms and conditions set forth hereinafter. - -Besides, if the Licensor owns or comes to own one or more patents -protecting all or part of the functions of the Software or of its -components, the Licensor undertakes not to enforce the rights granted by -these patents against successive Licensees using, exploiting or -modifying the Software. If these patents are transferred, the Licensor -undertakes to have the transferees subscribe to the obligations set -forth in this paragraph. - - - 5.1 RIGHT OF USE - -The Licensee is authorized to use the Software, without any limitation -as to its fields of application, with it being hereinafter specified -that this comprises: - - 1. permanent or temporary reproduction of all or part of the Software - by any or all means and in any or all form. - - 2. loading, displaying, running, or storing the Software on any or - all medium. - - 3. entitlement to observe, study or test its operation so as to - determine the ideas and principles behind any or all constituent - elements of said Software. This shall apply when the Licensee - carries out any or all loading, displaying, running, transmission - or storage operation as regards the Software, that it is entitled - to carry out hereunder. - - - 5.2 ENTITLEMENT TO MAKE CONTRIBUTIONS - -The right to make Contributions includes the right to translate, adapt, -arrange, or make any or all modifications to the Software, and the right -to reproduce the resulting software. - -The Licensee is authorized to make any or all Contributions to the -Software provided that it includes an explicit notice that it is the -author of said Contribution and indicates the date of the creation thereof. - - - 5.3 RIGHT OF DISTRIBUTION - -In particular, the right of distribution includes the right to publish, -transmit and communicate the Software to the general public on any or -all medium, and by any or all means, and the right to market, either in -consideration of a fee, or free of charge, one or more copies of the -Software by any means. - -The Licensee is further authorized to distribute copies of the modified -or unmodified Software to third parties according to the terms and -conditions set forth hereinafter. - - - 5.3.1 DISTRIBUTION OF SOFTWARE WITHOUT MODIFICATION - -The Licensee is authorized to distribute true copies of the Software in -Source Code or Object Code form, provided that said distribution -complies with all the provisions of the Agreement and is accompanied by: - - 1. a copy of the Agreement, - - 2. a notice relating to the limitation of both the Licensor's - warranty and liability as set forth in Articles 8 and 9, - -and that, in the event that only the Object Code of the Software is -redistributed, the Licensee allows effective access to the full Source -Code of the Software at a minimum during the entire period of its -distribution of the Software, it being understood that the additional -cost of acquiring the Source Code shall not exceed the cost of -transferring the data. - - - 5.3.2 DISTRIBUTION OF MODIFIED SOFTWARE - -If the Licensee makes any Contribution to the Software, the resulting -Modified Software may be distributed under a license agreement other -than this Agreement subject to compliance with the provisions of Article -5.3.4. - - - 5.3.3 DISTRIBUTION OF EXTERNAL MODULES - -When the Licensee has developed an External Module, the terms and -conditions of this Agreement do not apply to said External Module, that -may be distributed under a separate license agreement. - - - 5.3.4 CREDITS - -Any Licensee who may distribute a Modified Software hereby expressly -agrees to: - - 1. indicate in the related documentation that it is based on the - Software licensed hereunder, and reproduce the intellectual - property notice for the Software, - - 2. ensure that written indications of the Software intended use, - intellectual property notice and license hereunder are included in - easily accessible format from the Modified Software interface, - - 3. mention, on a freely accessible website describing the Modified - Software, at least throughout the distribution term thereof, that - it is based on the Software licensed hereunder, and reproduce the - Software intellectual property notice, - - 4. where it is distributed to a third party that may distribute a - Modified Software without having to make its source code - available, make its best efforts to ensure that said third party - agrees to comply with the obligations set forth in this Article . - -If the Software, whether or not modified, is distributed with an -External Module designed for use in connection with the Software, the -Licensee shall submit said External Module to the foregoing obligations. - - - 5.3.5 COMPATIBILITY WITH THE CeCILL AND CeCILL-C LICENSES - -Where a Modified Software contains a Contribution subject to the CeCILL -license, the provisions set forth in Article 5.3.4 shall be optional. - -A Modified Software may be distributed under the CeCILL-C license. In -such a case the provisions set forth in Article 5.3.4 shall be optional. - - - Article 6 - INTELLECTUAL PROPERTY - - - 6.1 OVER THE INITIAL SOFTWARE - -The Holder owns the economic rights over the Initial Software. Any or -all use of the Initial Software is subject to compliance with the terms -and conditions under which the Holder has elected to distribute its work -and no one shall be entitled to modify the terms and conditions for the -distribution of said Initial Software. - -The Holder undertakes that the Initial Software will remain ruled at -least by this Agreement, for the duration set forth in Article 4.2. - - - 6.2 OVER THE CONTRIBUTIONS - -The Licensee who develops a Contribution is the owner of the -intellectual property rights over this Contribution as defined by -applicable law. - - - 6.3 OVER THE EXTERNAL MODULES - -The Licensee who develops an External Module is the owner of the -intellectual property rights over this External Module as defined by -applicable law and is free to choose the type of agreement that shall -govern its distribution. - - - 6.4 JOINT PROVISIONS - -The Licensee expressly undertakes: - - 1. not to remove, or modify, in any manner, the intellectual property - notices attached to the Software; - - 2. to reproduce said notices, in an identical manner, in the copies - of the Software modified or not. - -The Licensee undertakes not to directly or indirectly infringe the -intellectual property rights of the Holder and/or Contributors on the -Software and to take, where applicable, vis-à-vis its staff, any and all -measures required to ensure respect of said intellectual property rights -of the Holder and/or Contributors. - - - Article 7 - RELATED SERVICES - -7.1 Under no circumstances shall the Agreement oblige the Licensor to -provide technical assistance or maintenance services for the Software. - -However, the Licensor is entitled to offer this type of services. The -terms and conditions of such technical assistance, and/or such -maintenance, shall be set forth in a separate instrument. Only the -Licensor offering said maintenance and/or technical assistance services -shall incur liability therefor. - -7.2 Similarly, any Licensor is entitled to offer to its licensees, under -its sole responsibility, a warranty, that shall only be binding upon -itself, for the redistribution of the Software and/or the Modified -Software, under terms and conditions that it is free to decide. Said -warranty, and the financial terms and conditions of its application, -shall be subject of a separate instrument executed between the Licensor -and the Licensee. - - - Article 8 - LIABILITY - -8.1 Subject to the provisions of Article 8.2, the Licensee shall be -entitled to claim compensation for any direct loss it may have suffered -from the Software as a result of a fault on the part of the relevant -Licensor, subject to providing evidence thereof. - -8.2 The Licensor's liability is limited to the commitments made under -this Agreement and shall not be incurred as a result of in particular: -(i) loss due the Licensee's total or partial failure to fulfill its -obligations, (ii) direct or consequential loss that is suffered by the -Licensee due to the use or performance of the Software, and (iii) more -generally, any consequential loss. In particular the Parties expressly -agree that any or all pecuniary or business loss (i.e. loss of data, -loss of profits, operating loss, loss of customers or orders, -opportunity cost, any disturbance to business activities) or any or all -legal proceedings instituted against the Licensee by a third party, -shall constitute consequential loss and shall not provide entitlement to -any or all compensation from the Licensor. - - - Article 9 - WARRANTY - -9.1 The Licensee acknowledges that the scientific and technical -state-of-the-art when the Software was distributed did not enable all -possible uses to be tested and verified, nor for the presence of -possible defects to be detected. In this respect, the Licensee's -attention has been drawn to the risks associated with loading, using, -modifying and/or developing and reproducing the Software which are -reserved for experienced users. - -The Licensee shall be responsible for verifying, by any or all means, -the suitability of the product for its requirements, its good working -order, and for ensuring that it shall not cause damage to either persons -or properties. - -9.2 The Licensor hereby represents, in good faith, that it is entitled -to grant all the rights over the Software (including in particular the -rights set forth in Article 5). - -9.3 The Licensee acknowledges that the Software is supplied "as is" by -the Licensor without any other express or tacit warranty, other than -that provided for in Article 9.2 and, in particular, without any warranty -as to its commercial value, its secured, safe, innovative or relevant -nature. - -Specifically, the Licensor does not warrant that the Software is free -from any error, that it will operate without interruption, that it will -be compatible with the Licensee's own equipment and software -configuration, nor that it will meet the Licensee's requirements. - -9.4 The Licensor does not either expressly or tacitly warrant that the -Software does not infringe any third party intellectual property right -relating to a patent, software or any other property right. Therefore, -the Licensor disclaims any and all liability towards the Licensee -arising out of any or all proceedings for infringement that may be -instituted in respect of the use, modification and redistribution of the -Software. Nevertheless, should such proceedings be instituted against -the Licensee, the Licensor shall provide it with technical and legal -assistance for its defense. Such technical and legal assistance shall be -decided on a case-by-case basis between the relevant Licensor and the -Licensee pursuant to a memorandum of understanding. The Licensor -disclaims any and all liability as regards the Licensee's use of the -name of the Software. No warranty is given as regards the existence of -prior rights over the name of the Software or as regards the existence -of a trademark. - - - Article 10 - TERMINATION - -10.1 In the event of a breach by the Licensee of its obligations -hereunder, the Licensor may automatically terminate this Agreement -thirty (30) days after notice has been sent to the Licensee and has -remained ineffective. - -10.2 A Licensee whose Agreement is terminated shall no longer be -authorized to use, modify or distribute the Software. However, any -licenses that it may have granted prior to termination of the Agreement -shall remain valid subject to their having been granted in compliance -with the terms and conditions hereof. - - - Article 11 - MISCELLANEOUS - - - 11.1 EXCUSABLE EVENTS - -Neither Party shall be liable for any or all delay, or failure to -perform the Agreement, that may be attributable to an event of force -majeure, an act of God or an outside cause, such as defective -functioning or interruptions of the electricity or telecommunications -networks, network paralysis following a virus attack, intervention by -government authorities, natural disasters, water damage, earthquakes, -fire, explosions, strikes and labor unrest, war, etc. - -11.2 Any failure by either Party, on one or more occasions, to invoke -one or more of the provisions hereof, shall under no circumstances be -interpreted as being a waiver by the interested Party of its right to -invoke said provision(s) subsequently. - -11.3 The Agreement cancels and replaces any or all previous agreements, -whether written or oral, between the Parties and having the same -purpose, and constitutes the entirety of the agreement between said -Parties concerning said purpose. No supplement or modification to the -terms and conditions hereof shall be effective as between the Parties -unless it is made in writing and signed by their duly authorized -representatives. - -11.4 In the event that one or more of the provisions hereof were to -conflict with a current or future applicable act or legislative text, -said act or legislative text shall prevail, and the Parties shall make -the necessary amendments so as to comply with said act or legislative -text. All other provisions shall remain effective. Similarly, invalidity -of a provision of the Agreement, for any reason whatsoever, shall not -cause the Agreement as a whole to be invalid. - - - 11.5 LANGUAGE - -The Agreement is drafted in both French and English and both versions -are deemed authentic. - - - Article 12 - NEW VERSIONS OF THE AGREEMENT - -12.1 Any person is authorized to duplicate and distribute copies of this -Agreement. - -12.2 So as to ensure coherence, the wording of this Agreement is -protected and may only be modified by the authors of the License, who -reserve the right to periodically publish updates or new versions of the -Agreement, each with a separate number. These subsequent versions may -address new issues encountered by Free Software. - -12.3 Any Software distributed under a given version of the Agreement may -only be subsequently distributed under the same version of the Agreement -or a subsequent version. - - - Article 13 - GOVERNING LAW AND JURISDICTION - -13.1 The Agreement is governed by French law. The Parties agree to -endeavor to seek an amicable solution to any disagreements or disputes -that may arise during the performance of the Agreement. - -13.2 Failing an amicable solution within two (2) months as from their -occurrence, and unless emergency proceedings are necessary, the -disagreements or disputes shall be referred to the Paris Courts having -jurisdiction, by the more diligent Party. - - -Version 1.0 dated 2006-09-05. diff --git a/etc/ChangeLog b/etc/ChangeLog deleted file mode 100644 index 12d6ef4..0000000 --- a/etc/ChangeLog +++ /dev/null @@ -1,141 +0,0 @@ -07/09/2016 - compatibility with Coq 8.7 and several small fixes - - version 1.6.2 and upcomming version 1.7 - * Compatibility with Coq 8.7 - * Lost compatibility with Coq 8.4 - -07/09/2016 - compatibility with Coq 8.7 and several small fixes - - upcomming version 1.7 - * New Theorems: - dec_factor_theorem, abstract_context, - mul_bin_down, mul_bin_left - - * Renamings or replacements: - mul_Sm_binm -> mul_bin_diag - divn1 -> divz1 (in intdiv) - - * Generalized or extended: - ltngtP, contra_eq, contra_neq, odd_opp - - * Plugin: - ssrpattern: compose nicely with Tactic Notation - -25/08/2016 - refactoring of algC and complex in ssrnum - - upcomming version 1.7 - * ssrnum's interface numClosedFieldType factors some theory from - both complex and algC. Because of that Re, Im, 'i, conjC, n.-root - and sqrtC are not specialized to algC anymore. In case of - ambiguity, they should be instanciated with algC using typing - constraints. Moreoever all the lemmas from ssrnum that used to - be in algC (like conjCK), now take an extra nonmaximal implicit - argument (C : numClosedFieldType) which could break some proofs. - Additionally, ad-hoc constructions from complex.v like -*+ or - complex.Re are now deprecated and one should rely solely on the - ssrnum interface. The next revision might definietly hide those - constructions under a module. - - * Structures that change: - numClosedFieldType - - * Renamed and generalized definitions: - rootC -> nthroot - algRe -> Re - algIm -> Im - algCi -> imaginaryC - - * Renamed and generalized theorems: - Every theorem from ssrnum that used to be in algC - -24/11/2015 - major reorganization of the archive - version 1.6 - * Files split into subdirectories: ssreflect, algebra, fingroup, - solvable, field and character. In this way the user can decide - to compile only the subset of the Mathematical Components library - that is relevant to her. Note that this introduces a possible - incompatibility for users of the previous version. A replacement - scheme is suggested in the installation notes. - - * The archive is now open and based on git. Public mirror at: - https://github.com/math-comp/math-comp - - * Sources of the reference manual of the Ssreflect tactic language are - also open and available at: - https://github.com/math-comp/ssr-manual - Pull requests improving the documentation are welcome. - - * Renamings or replacements: - conjC_closed -> cfConjC_closed - class_transr -> class_eqP - cfclass_transl -> cfclass_transr - nontrivial_ideal -> proper_ideal - zchar_orthonormalP -> vchar_orthonormalP - - * Definitions that changed: - seq_sub - - * Statements that changed: - orbit_in_transl, orbit_sym, orbit_trans, orbit_transl, orbit_transr, - cfAut_char, cfConjC_char, invg_lcosets, lcoset_transl, - lcoset_transr, rcoset_transl, rcoset_transr, mem2_last, - bind_unless, unless_contra, all_and2, all_and3, all_and4, all_and5, - ltr0_neq0, ltr_prod, Zisometry_of_iso - - * New definitions: - adhoc_seq_sub_choiceMixin, adhoc_seq_sub_[choice|fin]Type - - * New theorems: - orbit_in_eqP, cards_draws, cfAut_lin_char, cfConjC_lin_char, - extend_cfConjC_subset, isometry_of_free, cfAutK, cfAutVK, - lcoset_eqP, rcoset_eqP, class_eqP, gFsub_trans, gFnorms, - gFchar_trans, gFnormal_trans, gFnorm_trans, mem2_seq1, - dvdn_fact, prime_above, subKr, subrI, subIr, subr0_eq, - divrI, divIr, divKr, divfI, divIf, divKf, impliesP, impliesPn, - unlessL, unlessR, unless_sym, unlessP (coercion), classicW, - ltr_prod_nat - - * New notation: "\unless C, P" - -12/03/2014 - split the archive in SSReflect and MathComp - version 1.5 - * With this release "ssreflect" has been split into two packages. - The Ssreflect one contains the proof language (plugin for Coq) and a - small set of core theory libraries about boolean, natural numbers, - sequences, decidable equality and finite types. The Mathematical - Components one contains advanced theory files covering a wider - spectrum of mathematics. - - * With respect to version 1.4 the proof language got a few new - features related to forward reasoning and some bugfixes. The - Mathematical Components library features 16 new theory files and in - particular: some field and Galois theory, advanced character theory - and a construction of algebraic numbers. - -05/09/2012 - ssreflect - version 1.4 - * With this release the plugin code received many bug fixes and the - existing libraries relevant updates. This release also includes - some new libraries on the following topics: rational numbers, - divisibility of integers, F-algebras, finite dimensional field - extensions and Euclidean division for polynomials over a ring. - - * The release includes a major code refactoring of the plugin for Coq - 8.4. In particular a documented ML API to access the pattern matching - facilities of Ssreflect from third party plugins has been introduced. - -14/03/2011 - ssreflect - version 1.3 - * The tactic language has been extended with several new features, - inspired by the five years of intensive use in our project. However we - have kept the core of the language unchanged; the new library compiles - with Ssreflect 1.2. Users of a Coq 8.2 toplevel statically linked - with Ssreflect 1.2 need to comment the Declare ML Module "ssreflect" - line in ssreflect.v to properly compile the 1.3 library. We will - continue supporting new releases of Coq in due course. - - * The new library adds general linear algebra (matrix rank, subspaces) - and all of the advanced finite group that was developed in the course - of completing the Local Analysis part of the Odd Order Theorem, - starting from the Sylow and Hall theorems and including full structure - theorems for abelian, extremal and extraspecial groups, and general - (modular) linear representation theory. - -14/08/2009 - ssreflect - version 1.2 - * No change log - -18/03/2008 - ssreflect - version 1.1 - * First public release diff --git a/etc/INSTALL.md b/etc/INSTALL.md deleted file mode 100644 index 4bc3a95..0000000 --- a/etc/INSTALL.md +++ /dev/null @@ -1,78 +0,0 @@ -# INSTALLATION PROCEDURE - -Users familiar with OPAM can use such tool to install Coq and the Mathematical Components library with commands like - - opam repo add coq-released http://coq.inria.fr/opam/released - opam install coq-mathcomp-fingroup - -This document is for users that installed Coq in another way, for example -compiling it from sources. - -## REQUIREMENTS - -Coq version 8.5 to 8.7.0 - -## BUILDING - -The Mathematical Components library is divided into various installation -units. On can install the entire library (compilation time is around 35 minutes) or only some of its units. - -In both cases, if Coq is not installed such that its binaries like `coqc` -and `coq_makefile` are in the PATH, then the COQBIN environment variable -must be set to point to the directory containing such binaries. -For example: - - export COQBIN=/home/user/coq/bin/ - -Now, to install the entire library, including the SSReflect proof language: - - cd mathcomp-1.6/mathcomp - make -j2 && make install - -If one wants to only install a few modules he should instead run make -inside the modules he wants to install *in the following order*: - - 1. ssreflect - 2. fingroup - 3. algebra - 4. solvable - 5. field - 6. character - -This means that one cannot install, say, algebra without having already -installed fingroup. An example: - - cd mathcomp-1.6/mathcomp - cd ssreflect && make -j2 && make install - cd ../fingroup && make -j2 && make install - -## CUSTOMIZATION OF THE PROOF GENERAL EMACS INTERFACE - -The `mathcomp/ssreflect/` directory comes with a small configuration file -`pg-ssr.el` to extend ProofGeneral (PG), a generic interface for -proof assistants based on the customizable text editor Emacs, to the -syntax of ssreflect. - -The >= 3.7 versions of ProofGeneral support this extension. - -- Following the installation instructions, unpack the sources of PG in -a directory, for instance /ProofGeneral-3.7, and add -the following line to your .emacs file. -Under Unix/MacOS: - - (load-file - "/ProofGeneral-3.7/generic/proof-site.el" ) - (load-file "/pg-ssr.el") - -Under Windows+Cygwin: - - (load-file - "C:\\\\ProofGeneral-3.7\\generic\\proof-site.el") - (load-file "\\pg-ssr.el") - -Where is the location of your own ProofGeneral -directory, and where is the location of your pg-ssr.el -file. - -Coq sources have a .v extension. Opening any .v file should -automatically launch ProofGeneral. diff --git a/etc/Makefile b/etc/Makefile deleted file mode 100644 index 5515da0..0000000 --- a/etc/Makefile +++ /dev/null @@ -1,6 +0,0 @@ -VERSION=$(shell git symbolic-ref --short HEAD | cut -d / -f 2) - -dist: - cd ..; git archive --format tar --prefix mathcomp-$(VERSION)/\ - -o mathcomp-$(VERSION).tar HEAD - cd ..; gzip -f -9 mathcomp-$(VERSION).tar diff --git a/etc/README b/etc/README deleted file mode 100644 index 4d33be7..0000000 --- a/etc/README +++ /dev/null @@ -1,40 +0,0 @@ - THE MATHEMATICAL COMPONENTS LIBRARY - ------------------------------------------ - - -DOCUMENTATION -============= - - The documentation of the ssreflect tactics, a brief - description of the mathematical components libraries - and a detailed list of the changes made in the releases - is available as an Inria Research Report at - - http://hal.inria.fr/inria-00258384 - - -AVAILABILITY -============ - - Ssreflect and the Mathematical Components library are available at: - http://math-comp.github.io/math-comp/ - - -THE DISCUSSION LIST -=================== - - The ssreflect list (ssreflect@msr-inria.inria.fr) is meant to be - a standard way to discuss about the ssreflect extension and the - mathematical components library. - - To subscribe visit: https://sympa.inria.fr/sympa/info/ssreflect - -LICENSING -========= - - This program is free software; you can redistribute it and/or modify - it under the terms of the CeCILL B FREE SOFTWARE LICENSE. - - You should have received a copy of the CeCILL B License with this - Kit, in the file named "CeCILL-B". - If not, visit http://www.cecill.info -- cgit v1.2.3