cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
228 stars 36 forks source link

AttributeError: 'Values' object has no attribute 'pep_references' #37

Closed JasonGross closed 3 years ago

JasonGross commented 3 years ago
AttributeError: 'Values' object has no attribute 'pep_references'
Exiting due to error.  Use "--traceback" to diagnose.
Please report errors to <docutils-users@lists.sf.net>.
Include "--traceback" output, Docutils version (0.17.1 [release]),
Python version (3.7.3), your OS type & version, and the
command line used.
make: *** [Makefile:1004: alectryon-html-done.timestamp] Error 1

https://github.com/HoTT/HoTT/runs/2369972229#step:6:2123

Is it safe to always run with --traceback? Is it suggested?

JasonGross commented 3 years ago

Maybe it's not so nondeterministic, it seems to happen every time now.

Traceback (most recent call last):
  File "etc/alectryon/alectryon.py", line 26, in <module>
    main()
  File "/github/workspace/etc/alectryon/alectryon/cli.py", line 662, in main
    process_pipelines(args)
  File "/github/workspace/etc/alectryon/alectryon/cli.py", line 651, in process_pipelines
    state = call_pipeline_step(step, state, ctx)
  File "/github/workspace/etc/alectryon/alectryon/cli.py", line 620, in call_pipeline_step
    return step(state, **{p: ctx[p] for p in params})
  File "/github/workspace/etc/alectryon/alectryon/cli.py", line 114, in gen_rstcoq_html
    RSTCoqParser, RSTCoqStandaloneReader)
  File "/github/workspace/etc/alectryon/alectryon/cli.py", line 105, in _gen_docutils_html
    enable_exit_status=True).decode("utf-8")
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/core.py", line 417, in publish_string
    enable_exit_status=enable_exit_status)
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/core.py", line 665, in publish_programmatically
    output = pub.publish(enable_exit_status=enable_exit_status)
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/core.py", line 218, in publish
    self.settings)
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/readers/__init__.py", line 72, in read
    self.parse()
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/readers/__init__.py", line 78, in parse
    self.parser.parse(self.input, document)
  File "/github/workspace/etc/alectryon/alectryon/docutils.py", line 495, in parse
    self.statemachine.run(lines, document, inliner=self.inliner)
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/parsers/rst/states.py", line 158, in run
    inliner.init_customizations(document.settings)
  File "/home/coq/.local/lib/python3.7/site-packages/docutils/parsers/rst/states.py", line 607, in init_customizations
    if settings.pep_references:
AttributeError: 'Values' object has no attribute 'pep_references'
make: *** [Makefile:1005: alectryon-html-done.timestamp] Error 1

https://github.com/HoTT/HoTT/runs/2386323130?check_suite_focus=true#step:6:2122 https://github.com/HoTT/HoTT/pull/1466

JasonGross commented 3 years ago

Is there a way to get the python traceback to also print function arguments?

JasonGross commented 3 years ago

Traceback with arguments: https://github.com/HoTT/HoTT/runs/2393729047?check_suite_focus=true#step:6:2122

JasonGross commented 3 years ago
And here's the tail of the full traceback ``` File "/github/workspace/etc/alectryon/alectryon/cli.py", line 621, in call_pipeline_step return step(state, **{p: ctx[p] for p in params}) ctx = {'fpath': './theories/Basics.v', 'fname': 'Basics.v', 'input': ['./theories/Basics.v', './theories/Basics/Notations.v', './theories/Basics/Utf8.v', './theories/Basics/Overture.v', './theories/Basics/PathGroupoids.v', './theories/Basics/UniverseLevel.v', './theories/Basics/Contractible.v', './theories/Basics/Equivalences.v', './theories/Basics/Decidable.v', './theories/Basics/Datatypes.v', './theories/Basics/Logic.v', './theories/Basics/Tactics.v', './theories/Basics/Nat.v', './theories/Basics/Trunc.v', './theories/Basics/Numeral.v', './theories/Basics/Decimal.v', './theories/Basics/Hexadecimal.v', './theories/WildCat.v', './theories/WildCat/Core.v', './theories/WildCat/UnitCat.v', './theories/WildCat/EmptyCat.v', './theories/WildCat/Prod.v', './theories/WildCat/Equiv.v', './theories/WildCat/Sum.v', './theories/WildCat/Forall.v', './theories/WildCat/Sigma.v', './theories/WildCat/Opposite.v', './theories/WildCat/Paths.v', './theories/WildCat/Type.v', './theories/WildCat/Induced.v', './theories/WildCat/EquivGpd.v', './theories/WildCat/FunctorCat.v', './theories/WildCat/Yoneda.v', './theories/WildCat/TwoOneCat.v', './theories/WildCat/NatTrans.v', './theories/WildCat/PointedCat.v', './theories/WildCat/Square.v', './theories/Types.v', './theories/Types/Paths.v', './theories/Types/Unit.v', './theories/Types/Forall.v', './theories/Types/Arrow.v', './theories/Types/Sigma.v', './theories/Types/Prod.v', './theories/Types/Empty.v', './theories/Types/Bool.v', './theories/Types/Sum.v', './theories/Types/Wtype.v', './theories/Types/Equiv.v', './theories/Types/Universe.v', './theories/Cubical.v', './theories/Cubical/DPath.v', './theories/Cubical/PathSquare.v', './theories/Cubical/DPathSquare.v', './theories/Cubical/PathCube.v', './theories/Cubical/DPathCube.v', './theories/Spaces/Nat.v', './theories/Spaces/List.v', './theories/Spaces/Cantor.v', './theories/Spaces/Finite/Fin.v', './theories/Spaces/Finite/FinNat.v', './theories/Spaces/Finite/FinInduction.v', './theories/Spaces/Finite/Finite.v', './theories/Spaces/Finite/FinSeq.v', './theories/Spaces/Finite/Tactics.v', './theories/Spaces/Finite.v', './theories/Spaces/Universe.v', './theories/Spaces/Card.v', './theories/Spaces/Circle.v', './theories/Spaces/TwoSphere.v', './theories/Spaces/Spheres.v', './theories/Spaces/Int.v', './theories/Spaces/Int/Core.v', './theories/Spaces/Int/Spec.v', './theories/Spaces/Int/Equiv.v', './theories/Spaces/Int/LoopExp.v', './theories/Spaces/Pos.v', './theories/Spaces/Pos/Core.v', './theories/Spaces/Pos/Spec.v', './theories/Spaces/BAut.v', './theories/Spaces/BAut/Cantor.v', './theories/Spaces/BAut/Bool.v', './theories/Spaces/BAut/Bool/IncoherentIdempotent.v', './theories/Spaces/BAut/Rigid.v', './theories/Spaces/No.v', './theories/Spaces/No/Core.v', './theories/Spaces/No/Negation.v', './theories/Spaces/No/Addition.v', './theories/Spaces/Torus/Torus.v', './theories/Spaces/Torus/TorusEquivCircles.v', './theories/Spaces/Torus/TorusHomotopy.v', './theories/Modalities/ReflectiveSubuniverse.v', './theories/Modalities/Modality.v', './theories/Modalities/Accessible.v', './theories/Modalities/Descent.v', './theories/Modalities/Separated.v', './theories/Modalities/Lex.v', './theories/Modalities/Topological.v', './theories/Modalities/Notnot.v', './theories/Modalities/Identity.v', './theories/Modalities/Localization.v', './theories/Modalities/Nullification.v', './theories/Modalities/Open.v', './theories/Modalities/Closed.v', './theories/Modalities/Fracture.v', './theories/Modalities/CoreflectiveSubuniverse.v', './theories/HIT/Coeq.v', './theories/HIT/FreeIntQuotient.v', './theories/HIT/Flattening.v', './theories/HIT/Interval.v', './theories/HIT/epi.v', './theories/HIT/unique_choice.v', './theories/HIT/surjective_factor.v', './theories/HIT/quotient.v', './theories/HIT/iso.v', './theories/HIT/SetCone.v', './theories/HIT/V.v', './theories/Limits/Limit.v', './theories/Limits/Equalizer.v', './theories/Limits/Pullback.v', './theories/Colimits/Pushout.v', './theories/Colimits/SpanPushout.v', './theories/Colimits/MappingCylinder.v', './theories/Colimits/Quotient.v', './theories/Colimits/Colimit.v', './theories/Colimits/Colimit_Sigma.v', './theories/Colimits/Colimit_Prod.v', './theories/Colimits/Colimit_Pushout.v', './theories/Colimits/Colimit_Coequalizer.v', './theories/Colimits/Colimit_Flattening.v', './theories/Colimits/Colimit_Pushout_Flattening.v', './theories/Colimits/Sequential.v', './theories/Diagrams/Graph.v', './theories/Diagrams/Diagram.v', './theories/Diagrams/Cone.v', './theories/Diagrams/Cocone.v', './theories/Diagrams/DDiagram.v', './theories/Diagrams/ConstantDiagram.v', './theories/Diagrams/CommutativeSquares.v', './theories/Diagrams/Sequence.v', './theories/Diagrams/Span.v', './theories/Diagrams/ParallelPair.v', './theories/Truncations.v', './theories/Truncations/Core.v', './theories/Truncations/Connectedness.v', './theories/Equiv/BiInv.v', './theories/Equiv/PathSplit.v', './theories/Equiv/Relational.v', './theories/BoundedSearch.v', './theories/HFiber.v', './theories/HProp.v', './theories/Extensions.v', './theories/HSet.v', './theories/Projective.v', './theories/TruncType.v', './theories/DProp.v', './theories/EquivGroupoids.v', './theories/Functorish.v', './theories/FunextAxiom.v', './theories/UnivalenceAxiom.v', './theories/ObjectClassifier.v', './theories/NullHomotopy.v', './theories/Idempotents.v', './theories/Factorization.v', './theories/Constant.v', './theories/ExcludedMiddle.v', './theories/Misc.v', './theories/PathAny.v', './theories/Utf8.v', './theories/HoTT.v', './theories/Tests.v', './theories/Metatheory/Core.v', './theories/Metatheory/FunextVarieties.v', './theories/Metatheory/TruncImpliesFunext.v', './theories/Metatheory/IntervalImpliesFunext.v', './theories/Metatheory/UnivalenceImpliesFunext.v', './theories/Metatheory/UnivalenceVarieties.v', './theories/Homotopy/HomotopyGroup.v', './theories/Homotopy/Pi1S1.v', './theories/Homotopy/Suspension.v', './theories/Homotopy/Smash.v', './theories/Homotopy/Wedge.v', './theories/Homotopy/Join.v', './theories/Homotopy/WhiteheadsPrinciple.v', './theories/Homotopy/HSpace.v', './theories/Homotopy/HSpaceS1.v', './theories/Homotopy/BlakersMassey.v', './theories/Homotopy/Freudenthal.v', './theories/Homotopy/ClassifyingSpace.v', './theories/Homotopy/EMSpace.v', './theories/Homotopy/CayleyDickson.v', './theories/Homotopy/SuccessorStructure.v', './theories/Homotopy/ExactSequence.v', './theories/Pointed.v', './theories/Pointed/Core.v', './theories/Pointed/Loops.v', './theories/Pointed/pMap.v', './theories/Pointed/pFiber.v', './theories/Pointed/pEquiv.v', './theories/Pointed/pTrunc.v', './theories/Pointed/pHomotopy.v', './theories/Pointed/pSusp.v', './theories/Spectra/Spectrum.v', './theories/Spectra/Coinductive.v', './theories/Algebra/Universal/Algebra.v', './theories/Algebra/Universal/Homomorphism.v', './theories/Algebra/Universal/Operation.v', './theories/Algebra/Universal/Congruence.v', './theories/Algebra/Universal/TermAlgebra.v', './theories/Algebra/ooGroup.v', './theories/Algebra/Aut.v', './theories/Algebra/ooAction.v', './theories/Algebra/Congruence.v', './theories/Algebra/Rings.v', './theories/Algebra/Rings/CRing.v', './theories/Algebra/Rings/Ideal.v', './theories/Algebra/Rings/QuotientRing.v', './theories/Algebra/Rings/Z.v', './theories/Algebra/AbGroups.v', './theories/Algebra/AbGroups/AbelianGroup.v', './theories/Algebra/AbGroups/Abelianization.v', './theories/Algebra/AbGroups/AbPullback.v', './theories/Algebra/AbGroups/AbPushout.v', './theories/Algebra/AbGroups/Z.v', './theories/Algebra/Groups.v', './theories/Algebra/Groups/Group.v', './theories/Algebra/Groups/Subgroup.v', './theories/Algebra/Groups/QuotientGroup.v', './theories/Algebra/Groups/Image.v', './theories/Algebra/Groups/Kernel.v', './theories/Algebra/Groups/GrpPullback.v', './theories/Algebra/Groups/FreeProduct.v', './theories/Algebra/Groups/GroupCoeq.v', './theories/Algebra/Groups/Presentation.v', './theories/Algebra/Groups/ShortExactSequence.v', './theories/Algebra/Groups/FreeGroup.v', './theories/Algebra/Groups/FreeGroup/ListQuotient.v', './theories/Algebra/Groups/FreeGroup/LoopSusp.v', './theories/Tactics.v', './theories/Tactics/BinderApply.v', './theories/Tactics/EquivalenceInduction.v', './theories/Tactics/EvalIn.v', './theories/Tactics/Nameless.v', './theories/Tactics/RewriteModuloAssociativity.v', './theories/PropResizing/PropResizing.v', './theories/PropResizing/ImpredicativeTruncation.v', './theories/PropResizing/Nat.v', './theories/Classes/tactics/ring_tac.v', './theories/Classes/tactics/ring_quote.v', './theories/Classes/tactics/ring_pol.v', './theories/Classes/isomorphisms/rings.v', './theories/Classes/orders/rings.v', './theories/Classes/orders/maps.v', './theories/Classes/orders/semirings.v', './theories/Classes/orders/dec_fields.v', './theories/Classes/orders/sum.v', './theories/Classes/orders/lattices.v', './theories/Classes/orders/naturals.v', './theories/Classes/orders/orders.v', './theories/Classes/orders/nat_int.v', './theories/Classes/orders/integers.v', './theories/Classes/orders/archimedean.v', './theories/Classes/orders/fields.v', './theories/Classes/implementations/assume_rationals.v', './theories/Classes/implementations/peano_naturals.v', './theories/Classes/implementations/binary_naturals.v', './theories/Classes/implementations/natpair_integers.v', './theories/Classes/implementations/field_of_fractions.v', './theories/Classes/implementations/list.v', './theories/Classes/implementations/bool.v', './theories/Classes/implementations/hprop_lattice.v', './theories/Classes/implementations/pointwise.v', './theories/Classes/implementations/family_prod.v', './theories/Classes/implementations/ne_list.v', './theories/Classes/interfaces/monad.v', './theories/Classes/interfaces/abstract_algebra.v', './theories/Classes/interfaces/naturals.v', './theories/Classes/interfaces/rationals.v', './theories/Classes/interfaces/canonical_names.v', './theories/Classes/interfaces/orders.v', './theories/Classes/interfaces/archimedean.v', './theories/Classes/interfaces/cauchy.v', './theories/Classes/interfaces/round.v', './theories/Classes/interfaces/integers.v', './theories/Classes/interfaces/ua_algebra.v', './theories/Classes/interfaces/ua_setalgebra.v', './theories/Classes/interfaces/ua_congruence.v', './theories/Classes/theory/premetric.v', './theories/Classes/theory/int_abs.v', './theories/Classes/theory/rings.v', './theories/Classes/theory/additional_operations.v', './theories/Classes/theory/apartness.v', './theories/Classes/theory/dec_fields.v', './theories/Classes/theory/lattices.v', './theories/Classes/theory/naturals.v', './theories/Classes/theory/nat_distance.v', './theories/Classes/theory/groups.v', './theories/Classes/theory/fields.v', './theories/Classes/theory/rationals.v', './theories/Classes/theory/integers.v', './theories/Classes/theory/ua_homomorphism.v', './theories/Classes/theory/ua_isomorphic.v', './theories/Classes/theory/ua_prod_algebra.v', './theories/Classes/theory/ua_subalgebra.v', './theories/Classes/theory/ua_quotient_algebra.v', './theories/Classes/theory/ua_first_isomorphism.v', './theories/Classes/theory/ua_second_isomorphism.v', './theories/Classes/theory/ua_third_isomorphism.v', './theories/Classes/categories/ua_category.v', './theories/Classes/tests/ring_tac.v', './theories/Analysis/Locator.v', './theories/Categories.v', './theories/Categories/Category.v', './theories/Categories/Functor.v', './theories/Categories/NaturalTransformation.v', './theories/Categories/Category/Core.v', './theories/Categories/Functor/Core.v', './theories/Categories/NaturalTransformation/Core.v', './theories/Categories/Category/Morphisms.v', './theories/Categories/Category/Strict.v', './theories/Categories/Category/Univalent.v', './theories/Categories/Category/Objects.v', './theories/Categories/Category/Dual.v', './theories/Categories/Category/Paths.v', './theories/Categories/Category/Prod.v', './theories/Categories/Category/Pi.v', './theories/Categories/Category/Sum.v', './theories/Categories/Category/Sigma.v', './theories/Categories/Category/Sigma/Core.v', './theories/Categories/Functor/Composition.v', './theories/Categories/Functor/Composition/Core.v', './theories/Categories/Functor/Identity.v', './theories/Categories/Functor/Paths.v', './theories/Categories/Category/Sigma/OnMorphisms.v', './theories/Categories/Category/Sigma/OnObjects.v', './theories/Categories/Category/Sigma/Univalent.v', './theories/Categories/Category/Subcategory.v', './theories/Categories/Category/Subcategory/Full.v', './theories/Categories/Category/Subcategory/Wide.v', './theories/Categories/Category/Notations.v', './theories/Categories/Category/Utf8.v', './theories/Categories/Functor/Prod.v', './theories/Categories/Functor/Dual.v', './theories/Categories/SetCategory.v', './theories/Categories/SetCategory/Core.v', './theories/Categories/SetCategory/Morphisms.v', './theories/Categories/SetCategory/Functors.v', './theories/Categories/SetCategory/Functors/SetProp.v', './theories/Categories/SimplicialSets.v', './theories/Categories/SemiSimplicialSets.v', './theories/Categories/FundamentalPreGroupoidCategory.v', './theories/Categories/HomotopyPreCategory.v', './theories/Categories/HomFunctor.v', './theories/Categories/Functor/Attributes.v', './theories/Categories/NaturalTransformation/Paths.v', './theories/Categories/NaturalTransformation/Identity.v', './theories/Categories/NaturalTransformation/Composition.v', './theories/Categories/NaturalTransformation/Composition/Core.v', './theories/Categories/NaturalTransformation/Composition/Laws.v', './theories/Categories/FunctorCategory.v', './theories/Categories/FunctorCategory/Core.v', './theories/Categories/NaturalTransformation/Composition/Functorial.v', './theories/Categories/ExponentialLaws.v', './theories/Categories/ExponentialLaws/Law0.v', './theories/Categories/ExponentialLaws/Law1.v', './theories/Categories/ExponentialLaws/Law1/Functors.v', './theories/Categories/ExponentialLaws/Law1/Law.v', './theories/Categories/ExponentialLaws/Law2.v', './theories/Categories/ExponentialLaws/Law2/Functors.v', './theories/Categories/ExponentialLaws/Law2/Law.v', './theories/Categories/ExponentialLaws/Law3.v', './theories/Categories/ExponentialLaws/Law3/Functors.v', './theories/Categories/ExponentialLaws/Law3/Law.v', './theories/Categories/ExponentialLaws/Law4.v', './theories/Categories/ExponentialLaws/Law4/Functors.v', './theories/Categories/ExponentialLaws/Law4/Law.v', './theories/Categories/ExponentialLaws/Tactics.v', './theories/Categories/Functor/Composition/Functorial.v', './theories/Categories/Functor/Composition/Functorial/Core.v', './theories/Categories/Functor/Composition/Functorial/Attributes.v', './theories/Categories/Functor/Composition/Laws.v', './theories/Categories/Functor/Sum.v', './theories/Categories/Functor/Pointwise.v', './theories/Categories/Functor/Prod/Core.v', './theories/Categories/Functor/Prod/Universal.v', './theories/Categories/GroupoidCategory.v', './theories/Categories/GroupoidCategory/Core.v', './theories/Categories/GroupoidCategory/Dual.v', './theories/Categories/CategoryOfGroupoids.v', './theories/Categories/DiscreteCategory.v', './theories/Categories/IndiscreteCategory.v', './theories/Categories/NatCategory.v', './theories/Categories/ChainCategory.v', './theories/Categories/InitialTerminalCategory.v', './theories/Categories/InitialTerminalCategory/Core.v', './theories/Categories/InitialTerminalCategory/Functors.v', './theories/Categories/InitialTerminalCategory/NaturalTransformations.v', './theories/Categories/InitialTerminalCategory/Pseudofunctors.v', './theories/Categories/InitialTerminalCategory/Notations.v', './theories/Categories/NaturalTransformation/Prod.v', './theories/Categories/Functor/Prod/Functorial.v', './theories/Categories/Functor/Pointwise/Core.v', './theories/Categories/Functor/Pointwise/Properties.v', './theories/Categories/Functor/Notations.v', './theories/Categories/Functor/Utf8.v', './theories/Categories/NaturalTransformation/Dual.v', './theories/Categories/NaturalTransformation/Sum.v', './theories/Categories/NaturalTransformation/Pointwise.v', './theories/Categories/FunctorCategory/Dual.v', './theories/Categories/FunctorCategory/Morphisms.v', './theories/Categories/NaturalTransformation/Isomorphisms.v', './theories/Categories/NaturalTransformation/Notations.v', './theories/Categories/NaturalTransformation/Utf8.v', './theories/Categories/Structure.v', './theories/Categories/Structure/Core.v', './theories/Categories/Structure/IdentityPrinciple.v', './theories/Categories/Structure/Notations.v', './theories/Categories/Structure/Utf8.v', './theories/Categories/CategoryOfSections.v', './theories/Categories/CategoryOfSections/Core.v', './theories/Categories/Profunctor/Core.v', './theories/Categories/Profunctor/Identity.v', './theories/Categories/Comma.v', './theories/Categories/Comma/Core.v', './theories/Categories/Adjoint.v', './theories/Categories/Adjoint/UnitCounit.v', './theories/Categories/Adjoint/Core.v', './theories/Categories/Adjoint/Paths.v', './theories/Categories/Adjoint/Identity.v', './theories/Categories/Adjoint/Composition.v', './theories/Categories/Adjoint/Composition/Core.v', './theories/Categories/Adjoint/Composition/LawsTactic.v', './theories/Categories/Adjoint/Composition/AssociativityLaw.v', './theories/Categories/Adjoint/Composition/IdentityLaws.v', './theories/Categories/Adjoint/Dual.v', './theories/Categories/Adjoint/UnitCounitCoercions.v', './theories/Categories/Adjoint/UniversalMorphisms.v', './theories/Categories/Adjoint/UniversalMorphisms/Core.v', './theories/Categories/Adjoint/Functorial.v', './theories/Categories/Adjoint/Functorial/Core.v', './theories/Categories/Adjoint/Functorial/Parts.v', './theories/Categories/Adjoint/Functorial/Laws.v', './theories/Categories/Adjoint/Hom.v', './theories/Categories/Adjoint/HomCoercions.v', './theories/Categories/Adjoint/Pointwise.v', './theories/Categories/Adjoint/Notations.v', './theories/Categories/Adjoint/Utf8.v', './theories/Categories/Cat.v', './theories/Categories/Cat/Core.v', './theories/Categories/DualFunctor.v', './theories/Categories/FunctorCategory/Functorial.v', './theories/Categories/FunctorCategory/Notations.v', './theories/Categories/FunctorCategory/Utf8.v', './theories/Categories/ProductLaws.v', './theories/Categories/GroupoidCategory/Morphisms.v', './theories/Categories/Profunctor.v', './theories/Categories/Profunctor/Representable.v', './theories/Categories/Profunctor/Notations.v', './theories/Categories/Profunctor/Utf8.v', './theories/Categories/Yoneda.v', './theories/Categories/Cat/Morphisms.v', './theories/Categories/Comma/Dual.v', './theories/Categories/Comma/Projection.v', './theories/Categories/Comma/InducedFunctors.v', './theories/Categories/Comma/ProjectionFunctors.v', './theories/Categories/Comma/Functorial.v', './theories/Categories/Comma/Notations.v', './theories/Categories/Comma/Utf8.v', './theories/Categories/Pseudofunctor.v', './theories/Categories/Pseudofunctor/Core.v', './theories/Categories/Pseudofunctor/RewriteLaws.v', './theories/Categories/Pseudofunctor/FromFunctor.v', './theories/Categories/Pseudofunctor/Identity.v', './theories/Categories/PseudonaturalTransformation.v', './theories/Categories/PseudonaturalTransformation/Core.v', './theories/Categories/LaxComma.v', './theories/Categories/LaxComma/Core.v', './theories/Categories/LaxComma/CoreParts.v', './theories/Categories/LaxComma/CoreLaws.v', './theories/Categories/LaxComma/Notations.v', './theories/Categories/LaxComma/Utf8.v', './theories/Categories/Grothendieck.v', './theories/Categories/Grothendieck/ToSet.v', './theories/Categories/Grothendieck/ToSet/Core.v', './theories/Categories/Grothendieck/ToSet/Morphisms.v', './theories/Categories/Grothendieck/ToSet/Univalent.v', './theories/Categories/Grothendieck/PseudofunctorToCat.v', './theories/Categories/Grothendieck/ToCat.v', './theories/Categories/DependentProduct.v', './theories/Categories/UniversalProperties.v', './theories/Categories/KanExtensions.v', './theories/Categories/KanExtensions/Core.v', './theories/Categories/KanExtensions/Functors.v', './theories/Categories/Limits.v', './theories/Categories/Limits/Core.v', './theories/Categories/Limits/Functors.v', './theories/Categories/Notations.v', './theories/Categories/Utf8.v', './contrib/HoTTBook.v', './contrib/HoTTBookExercises.v'], 'stdin_filename': None, 'frontend': 'coq+rst', 'backend': 'webpage', 'output': None, 'output_directory': 'alectryon-html', 'copy_fn': , 'cache_directory': 'alectryon-cache', 'include_banner': 'True', 'include_vernums': True, 'webpage_style': 'centered', 'mark_point': (None, None), 'sertop_args': ['--no_prelude', '--indices-matter', '-R', './theories,HoTT', '-Q', './contrib,HoTT.Contrib'], 'coq_args_I': [], 'coq_args_Q': [['./contrib', 'HoTT.Contrib']], 'coq_args_R': [['./theories', 'HoTT']], 'debug': False, 'traceback': True, 'point': None, 'marker': None, 'html_assets': ['alectryon.js', 'alectryon.css', 'docutils_basic.css', 'tango_subtle.css', 'tango_subtle.min.css'], 'html_classes': [], 'pipelines': [('./theories/Basics.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Notations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Utf8.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Overture.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/PathGroupoids.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/UniverseLevel.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Contractible.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Equivalences.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Decidable.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Datatypes.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Logic.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Tactics.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Nat.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Trunc.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Numeral.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Decimal.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Basics/Hexadecimal.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/UnitCat.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/EmptyCat.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Prod.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Equiv.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Sum.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Forall.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Sigma.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Opposite.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Paths.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Type.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Induced.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/EquivGpd.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/FunctorCat.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Yoneda.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/TwoOneCat.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/NatTrans.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/PointedCat.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/WildCat/Square.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Types.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Types/Paths.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Types/Unit.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Types/Forall.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Types/Arrow.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Types/Sigma.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Types/Prod.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Types/Empty.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Types/Bool.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Types/Sum.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Types/Wtype.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Types/Equiv.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Types/Universe.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Cubical.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Cubical/DPath.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Cubical/PathSquare.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Cubical/DPathSquare.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Cubical/PathCube.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Cubical/DPathCube.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Nat.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/List.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Cantor.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite/Fin.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite/FinNat.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite/FinInduction.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite/Finite.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite/FinSeq.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite/Tactics.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Finite.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Universe.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Card.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Circle.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/TwoSphere.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Spheres.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Int.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Int/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Int/Spec.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Int/Equiv.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Int/LoopExp.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Pos.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Pos/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Pos/Spec.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/BAut.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/BAut/Cantor.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/BAut/Bool.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/BAut/Bool/IncoherentIdempotent.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/BAut/Rigid.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/No.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/No/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/No/Negation.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/No/Addition.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Torus/Torus.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Torus/TorusEquivCircles.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spaces/Torus/TorusHomotopy.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/ReflectiveSubuniverse.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Modality.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Accessible.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Descent.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Separated.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Lex.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Topological.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Notnot.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Identity.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Localization.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Nullification.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Open.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Closed.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/Fracture.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Modalities/CoreflectiveSubuniverse.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HIT/Coeq.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HIT/FreeIntQuotient.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HIT/Flattening.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HIT/Interval.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HIT/epi.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HIT/unique_choice.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HIT/surjective_factor.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HIT/quotient.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HIT/iso.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HIT/SetCone.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HIT/V.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Limits/Limit.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Limits/Equalizer.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Limits/Pullback.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Pushout.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Colimits/SpanPushout.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Colimits/MappingCylinder.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Quotient.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit_Sigma.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit_Prod.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit_Pushout.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit_Coequalizer.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit_Flattening.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Colimit_Pushout_Flattening.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Colimits/Sequential.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/Graph.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/Diagram.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/Cone.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/Cocone.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/DDiagram.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/ConstantDiagram.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/CommutativeSquares.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/Sequence.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/Span.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Diagrams/ParallelPair.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Truncations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Truncations/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Truncations/Connectedness.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Equiv/BiInv.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Equiv/PathSplit.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Equiv/Relational.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/BoundedSearch.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HFiber.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HProp.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Extensions.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HSet.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Projective.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/TruncType.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/DProp.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/EquivGroupoids.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Functorish.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/FunextAxiom.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/UnivalenceAxiom.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/ObjectClassifier.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/NullHomotopy.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Idempotents.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Factorization.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Constant.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/ExcludedMiddle.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Misc.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/PathAny.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Utf8.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/HoTT.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Tests.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Metatheory/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Metatheory/FunextVarieties.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Metatheory/TruncImpliesFunext.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Metatheory/IntervalImpliesFunext.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Metatheory/UnivalenceImpliesFunext.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Metatheory/UnivalenceVarieties.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/HomotopyGroup.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/Pi1S1.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/Suspension.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/Smash.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/Wedge.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/Join.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/WhiteheadsPrinciple.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/HSpace.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/HSpaceS1.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/BlakersMassey.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/Freudenthal.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/ClassifyingSpace.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/EMSpace.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/CayleyDickson.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/SuccessorStructure.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Homotopy/ExactSequence.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Pointed.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Pointed/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Pointed/Loops.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Pointed/pMap.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Pointed/pFiber.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Pointed/pEquiv.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Pointed/pTrunc.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Pointed/pHomotopy.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Pointed/pSusp.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spectra/Spectrum.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Spectra/Coinductive.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Universal/Algebra.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Universal/Homomorphism.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Universal/Operation.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Universal/Congruence.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Universal/TermAlgebra.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/ooGroup.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Aut.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/ooAction.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Congruence.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Rings.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Rings/CRing.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Rings/Ideal.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Rings/QuotientRing.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Rings/Z.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/AbGroups.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/AbGroups/AbelianGroup.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/AbGroups/Abelianization.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/AbGroups/AbPullback.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/AbGroups/AbPushout.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/AbGroups/Z.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/Group.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/Subgroup.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/QuotientGroup.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/Image.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/Kernel.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/GrpPullback.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/FreeProduct.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/GroupCoeq.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/Presentation.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/ShortExactSequence.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/FreeGroup.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/FreeGroup/ListQuotient.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Algebra/Groups/FreeGroup/LoopSusp.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Tactics.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Tactics/BinderApply.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Tactics/EquivalenceInduction.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Tactics/EvalIn.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Tactics/Nameless.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Tactics/RewriteModuloAssociativity.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/PropResizing/PropResizing.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/PropResizing/ImpredicativeTruncation.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/PropResizing/Nat.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/tactics/ring_tac.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/tactics/ring_quote.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/tactics/ring_pol.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/isomorphisms/rings.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/rings.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/maps.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/semirings.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/dec_fields.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/sum.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/lattices.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/naturals.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/orders.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/nat_int.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/integers.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/archimedean.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/orders/fields.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/assume_rationals.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/peano_naturals.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/binary_naturals.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/natpair_integers.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/field_of_fractions.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/list.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/bool.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/hprop_lattice.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/pointwise.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/family_prod.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/implementations/ne_list.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/monad.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/abstract_algebra.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/naturals.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/rationals.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/canonical_names.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/orders.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/archimedean.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/cauchy.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/round.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/integers.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/ua_algebra.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/ua_setalgebra.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/interfaces/ua_congruence.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/premetric.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/int_abs.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/rings.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/additional_operations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/apartness.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/dec_fields.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/lattices.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/naturals.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/nat_distance.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/groups.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/fields.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/rationals.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/integers.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_homomorphism.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_isomorphic.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_prod_algebra.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_subalgebra.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_quotient_algebra.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_first_isomorphism.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_second_isomorphism.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/theory/ua_third_isomorphism.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/categories/ua_category.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Classes/tests/ring_tac.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Analysis/Locator.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Morphisms.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Strict.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Univalent.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Objects.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Dual.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Paths.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Prod.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Pi.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Sum.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Sigma.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Sigma/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Composition.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Composition/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Identity.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Paths.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Sigma/OnMorphisms.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Sigma/OnObjects.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Sigma/Univalent.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Subcategory.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Subcategory/Full.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Subcategory/Wide.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Notations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Category/Utf8.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Prod.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Dual.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/SetCategory.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/SetCategory/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/SetCategory/Morphisms.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/SetCategory/Functors.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/SetCategory/Functors/SetProp.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/SimplicialSets.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/SemiSimplicialSets.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/FundamentalPreGroupoidCategory.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/HomotopyPreCategory.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/HomFunctor.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Attributes.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Paths.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Identity.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Composition.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Composition/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Composition/Laws.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Composition/Functorial.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law0.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law1.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law1/Functors.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law1/Law.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law2.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law2/Functors.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law2/Law.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law3.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law3/Functors.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law3/Law.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law4.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law4/Functors.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Law4/Law.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ExponentialLaws/Tactics.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Composition/Functorial.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Composition/Functorial/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Composition/Functorial/Attributes.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Composition/Laws.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Sum.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Pointwise.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Prod/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Prod/Universal.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/GroupoidCategory.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/GroupoidCategory/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/GroupoidCategory/Dual.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/CategoryOfGroupoids.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/DiscreteCategory.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/IndiscreteCategory.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NatCategory.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ChainCategory.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/InitialTerminalCategory.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/InitialTerminalCategory/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/InitialTerminalCategory/Functors.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/InitialTerminalCategory/NaturalTransformations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/InitialTerminalCategory/Pseudofunctors.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/InitialTerminalCategory/Notations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Prod.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Prod/Functorial.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Pointwise/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Pointwise/Properties.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Notations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Functor/Utf8.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Dual.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Sum.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Pointwise.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory/Dual.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory/Morphisms.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Isomorphisms.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Notations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/NaturalTransformation/Utf8.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Structure.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Structure/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Structure/IdentityPrinciple.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Structure/Notations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Structure/Utf8.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/CategoryOfSections.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/CategoryOfSections/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Profunctor/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Profunctor/Identity.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/UnitCounit.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Paths.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Identity.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Composition.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Composition/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Composition/LawsTactic.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Composition/AssociativityLaw.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Composition/IdentityLaws.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Dual.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/UnitCounitCoercions.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/UniversalMorphisms.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/UniversalMorphisms/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Functorial.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Functorial/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Functorial/Parts.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Functorial/Laws.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Hom.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/HomCoercions.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Pointwise.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Notations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Adjoint/Utf8.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Cat.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Cat/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/DualFunctor.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory/Functorial.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory/Notations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/FunctorCategory/Utf8.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/ProductLaws.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/GroupoidCategory/Morphisms.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Profunctor.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Profunctor/Representable.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Profunctor/Notations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Profunctor/Utf8.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Yoneda.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Cat/Morphisms.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/Dual.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/Projection.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/InducedFunctors.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/ProjectionFunctors.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/Functorial.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/Notations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Comma/Utf8.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Pseudofunctor.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Pseudofunctor/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Pseudofunctor/RewriteLaws.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Pseudofunctor/FromFunctor.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Pseudofunctor/Identity.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/PseudonaturalTransformation.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/PseudonaturalTransformation/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/LaxComma.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/LaxComma/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/LaxComma/CoreParts.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/LaxComma/CoreLaws.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/LaxComma/Notations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/LaxComma/Utf8.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck/ToSet.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck/ToSet/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck/ToSet/Morphisms.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck/ToSet/Univalent.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck/PseudofunctorToCat.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Grothendieck/ToCat.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/DependentProduct.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/UniversalProperties.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/KanExtensions.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/KanExtensions/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/KanExtensions/Functors.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Limits.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Limits/Core.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Limits/Functors.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Notations.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./theories/Categories/Utf8.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./contrib/HoTTBook.v', (, , , , . at 0x7fafa4e3b7b8>)), ('./contrib/HoTTBookExercises.v', (, , , , . at 0x7fafa4e3b7b8>))]} params = ['fpath', 'webpage_style', 'include_banner', 'include_vernums', 'html_assets', 'traceback'] state = 'Require Export Basics.Notations.\nRequire Export Basics.Overture.\nRequire Export Basics.UniverseLevel.\nRequire Export Basics.PathGroupoids.\nRequire Export Basics.Contractible.\nRequire Export Basics.Equivalences.\nRequire Export Basics.Trunc.\nRequire Export Basics.Decidable.\nRequire Export Basics.Utf8.\nRequire Export Basics.Tactics.\n\nRequire Export Basics.Nat.\nRequire Export Basics.Numeral.\n' step = File "/github/workspace/etc/alectryon/alectryon/cli.py", line 115, in gen_rstcoq_html document = inliner = input_lines = StringList(['.. coq::', '', ' Require Export Basics.Notations.', ' Require Export Basics.Overture.', ' Require Export Basics.UniverseLevel.', ' Require Export Basics.PathGroupoids.', ' Require Export Basics.Contractible.', ' Require Export Basics.Equivalences.', ' Require Export Basics.Trunc.', ' Require Export Basics.Decidable.', ' Require Export Basics.Utf8.', ' Require Export Basics.Tactics.', '', ' Require Export Basics.Nat.', ' Require Export Basics.Numeral.', ''], items=[('./theories/Basics.v', 0), ('./theories/Basics.v', 0), ('./theories/Basics.v', 0), ('./theories/Basics.v', 1), ('./theories/Basics.v', 2), ('./theories/Basics.v', 3), ('./theories/Basics.v', 4), ('./theories/Basics.v', 5), ('./theories/Basics.v', 6), ('./theories/Basics.v', 7), ('./theories/Basics.v', 8), ('./theories/Basics.v', 9), ('./theories/Basics.v', 10), ('./theories/Basics.v', 11), ('./theories/Basics.v', 12), ('./theories/Basics.v', 12)]) input_offset = 0 match_titles = True self = File "/home/coq/.local/lib/python3.7/site-packages/docutils/parsers/rst/states.py", line 607, in init_customizations if settings.pep_references: args = {'self': , 'settings': , 'start_string_prefix': '(^|(?<=\\s|["\'(<\\[{༺༼᚛⁅⁽₍〈❨❪❬❮❰❲❴⟅⟦⟨⟪⟬⟮⦃⦅⦇⦉⦋⦍⦏⦑⦓⦕⦗⧘⧚⧼⸢⸤⸦⸨〈《「『【〔〖〘〚〝〝﴾︗︵︷︹︻︽︿﹁﹃﹇﹙﹛﹝([{⦅「«‘“‹⸂⸄⸉⸌⸜⸠‚„»’”›⸃⸅⸊⸍⸝⸡‛‟\\-/:֊¡·¿;·՚-՟։־׀׃׆׳״؉؊،؍؛؞؟٪-٭۔܀-܍߷-߹࠰-࠾।॥॰෴๏๚๛༄-༒྅࿐-࿔၊-၏჻፡-፨᐀᙭᙮᛫-᛭᜵᜶។-៖៘-៚᠀-᠊᥄᥅᧞᧟᨞᨟᪠-᪦᪨-᪭᭚-᭠᰻-᰿᱾᱿᳓‐-‗†-‧‰-‸※-‾⁁-⁃⁇-⁑⁓⁕-⁞⳹-⳼⳾⳿⸀⸁⸆-⸈⸋⸎-⸛⸞⸟⸪-⸮⸰⸱、-〃〜〰〽゠・꓾꓿꘍-꘏꙳꙾꛲-꛷꡴-꡷꣎꣏꣸-꣺꤮꤯꥟꧁-꧍꧞꧟꩜-꩟꫞꫟꯫︐-︖︙︰-︲﹅﹆﹉-﹌﹐-﹒﹔-﹘﹟-﹡﹣﹨﹪﹫!-#%-'*,-/:;?@\。、・𐄀𐄁𐎟𐏐𐡗𐤟𐤿𐩐-𐩘𐩿𐬹-𐬿𑂻𑂼𑂾-𑃁𒑰-𒑳]))', 'end_string_suffix': '($|(?=\\s|[\x00\\\\.,;!?\\-/:֊¡·¿;·՚-՟։־׀׃׆׳״؉؊،؍؛؞؟٪-٭۔܀-܍߷-߹࠰-࠾।॥॰෴๏๚๛༄-༒྅࿐-࿔၊-၏჻፡-፨᐀᙭᙮᛫-᛭᜵᜶។-៖៘-៚᠀-᠊᥄᥅᧞᧟᨞᨟᪠-᪦᪨-᪭᭚-᭠᰻-᰿᱾᱿᳓‐-‗†-‧‰-‸※-‾⁁-⁃⁇-⁑⁓⁕-⁞⳹-⳼⳾⳿⸀⸁⸆-⸈⸋⸎-⸛⸞⸟⸪-⸮⸰⸱、-〃〜〰〽゠・꓾꓿꘍-꘏꙳꙾꛲-꛷꡴-꡷꣎꣏꣸-꣺꤮꤯꥟꧁-꧍꧞꧟꩜-꩟꫞꫟꯫︐-︖︙︰-︲﹅﹆﹉-﹌﹐-﹒﹔-﹘﹟-﹡﹣﹨﹪﹫!-#%-'*,-/:;?@\。、・𐄀𐄁𐎟𐏐𐡗𐤟𐤿𐩐-𐩘𐩿𐬹-𐬿𑂻𑂼𑂾-𑃁𒑰-𒑳"\')>\\]}༻༽᚜⁆⁾₎〉❩❫❭❯❱❳❵⟆⟧⟩⟫⟭⟯⦄⦆⦈⦊⦌⦎⦐⦒⦔⦖⦘⧙⧛⧽⸣⸥⸧⸩〉》」』】〕〗〙〛〞〟﴿︘︶︸︺︼︾﹀﹂﹄﹈﹚﹜﹞)]}⦆」»’”›⸃⸅⸊⸍⸝⸡‛‟«‘“‹⸂⸄⸉⸌⸜⸠‚„]))', '__module__': 'docutils.parsers.rst.states', '__doc__': '\n Parse inline markup; call the `parse()` method.\n ', '__init__': , 'init_customizations': , 'parse': , 'non_whitespace_before': '(?]', 'urilast': '[_~*/=+a-zA-Z0-9]', 'uri_end': "(?:[_~*/=+a-zA-Z0-9]|[-_.!~*'()[\\];/:@&=+$,%a-zA-Z0-9\\x00](?=[>]))", 'emailc': "[-_!~*'{|}/#?^`&=+$%a-zA-Z0-9\\x00]", 'email_pattern': '\n %(emailc)s+(?:\\.%(emailc)s+)* # name\n (?, 'inline_obj': , 'problematic': , 'emphasis': , 'strong': , 'interpreted_or_phrase_ref': , 'phrase_ref': , 'adjust_uri': , 'interpreted': , 'literal': , 'inline_internal_target': , 'substitution_reference': , 'footnote_reference': , 'reference': , 'anonymous_reference': , 'standalone_uri': , 'pep_reference': , 'rfc_url': 'rfc%d.html', 'rfc_reference': , 'implicit_inline': , 'dispatch': {'*': , '**': , '`': , '``': , '_`': , ']_': , '|': , '_': , '__': }, '__dict__': , '__weakref__': } end_string_suffix = '($|(?=\\s|[\x00\\\\.,;!?\\-/:֊¡·¿;·՚-՟։־׀׃׆׳״؉؊،؍؛؞؟٪-٭۔܀-܍߷-߹࠰-࠾।॥॰෴๏๚๛༄-༒྅࿐-࿔၊-၏჻፡-፨᐀᙭᙮᛫-᛭᜵᜶។-៖៘-៚᠀-᠊᥄᥅᧞᧟᨞᨟᪠-᪦᪨-᪭᭚-᭠᰻-᰿᱾᱿᳓‐-‗†-‧‰-‸※-‾⁁-⁃⁇-⁑⁓⁕-⁞⳹-⳼⳾⳿⸀⸁⸆-⸈⸋⸎-⸛⸞⸟⸪-⸮⸰⸱、-〃〜〰〽゠・꓾꓿꘍-꘏꙳꙾꛲-꛷꡴-꡷꣎꣏꣸-꣺꤮꤯꥟꧁-꧍꧞꧟꩜-꩟꫞꫟꯫︐-︖︙︰-︲﹅﹆﹉-﹌﹐-﹒﹔-﹘﹟-﹡﹣﹨﹪﹫!-#%-'*,-/:;?@\。、・𐄀𐄁𐎟𐏐𐡗𐤟𐤿𐩐-𐩘𐩿𐬹-𐬿𑂻𑂼𑂾-𑃁𒑰-𒑳"\')>\\]}༻༽᚜⁆⁾₎〉❩❫❭❯❱❳❵⟆⟧⟩⟫⟭⟯⦄⦆⦈⦊⦌⦎⦐⦒⦔⦖⦘⧙⧛⧽⸣⸥⸧⸩〉》」』】〕〗〙〛〞〟﴿︘︶︸︺︼︾﹀﹂﹄﹈﹚﹜﹞)]}⦆」»’”›⸃⸅⸊⸍⸝⸡‛‟«‘“‹⸂⸄⸉⸌⸜⸠‚„]))' parts = ('initial_inline', '(^|(?<=\\s|["\'(<\\[{༺༼᚛⁅⁽₍〈❨❪❬❮❰❲❴⟅⟦⟨⟪⟬⟮⦃⦅⦇⦉⦋⦍⦏⦑⦓⦕⦗⧘⧚⧼⸢⸤⸦⸨〈《「『【〔〖〘〚〝〝﴾︗︵︷︹︻︽︿﹁﹃﹇﹙﹛﹝([{⦅「«‘“‹⸂⸄⸉⸌⸜⸠‚„»’”›⸃⸅⸊⸍⸝⸡‛‟\\-/:֊¡·¿;·՚-՟։־׀׃׆׳״؉؊،؍؛؞؟٪-٭۔܀-܍߷-߹࠰-࠾।॥॰෴๏๚๛༄-༒྅࿐-࿔၊-၏჻፡-፨᐀᙭᙮᛫-᛭᜵᜶។-៖៘-៚᠀-᠊᥄᥅᧞᧟᨞᨟᪠-᪦᪨-᪭᭚-᭠᰻-᰿᱾᱿᳓‐-‗†-‧‰-‸※-‾⁁-⁃⁇-⁑⁓⁕-⁞⳹-⳼⳾⳿⸀⸁⸆-⸈⸋⸎-⸛⸞⸟⸪-⸮⸰⸱、-〃〜〰〽゠・꓾꓿꘍-꘏꙳꙾꛲-꛷꡴-꡷꣎꣏꣸-꣺꤮꤯꥟꧁-꧍꧞꧟꩜-꩟꫞꫟꯫︐-︖︙︰-︲﹅﹆﹉-﹌﹐-﹒﹔-﹘﹟-﹡﹣﹨﹪﹫!-#%-'*,-/:;?@\。、・𐄀𐄁𐎟𐏐𐡗𐤟𐤿𐩐-𐩘𐩿𐬹-𐬿𑂻𑂼𑂾-𑃁𒑰-𒑳]))', '', [('start', '', '(?!\\s)', ['\\*\\*', '\\*(?!\\*)', '``', '_`', '\\|(?!\\|)']), ('whole', '', '($|(?=\\s|[\x00\\\\.,;!?\\-/:֊¡·¿;·՚-՟։־׀׃׆׳״؉؊،؍؛؞؟٪-٭۔܀-܍߷-߹࠰-࠾।॥॰෴๏๚๛༄-༒྅࿐-࿔၊-၏჻፡-፨᐀᙭᙮᛫-᛭᜵᜶។-៖៘-៚᠀-᠊᥄᥅᧞᧟᨞᨟᪠-᪦᪨-᪭᭚-᭠᰻-᰿᱾᱿᳓‐-‗†-‧‰-‸※-‾⁁-⁃⁇-⁑⁓⁕-⁞⳹-⳼⳾⳿⸀⸁⸆-⸈⸋⸎-⸛⸞⸟⸪-⸮⸰⸱、-〃〜〰〽゠・꓾꓿꘍-꘏꙳꙾꛲-꛷꡴-꡷꣎꣏꣸-꣺꤮꤯꥟꧁-꧍꧞꧟꩜-꩟꫞꫟꯫︐-︖︙︰-︲﹅﹆﹉-﹌﹐-﹒﹔-﹘﹟-﹡﹣﹨﹪﹫!-#%-'*,-/:;?@\。、・𐄀𐄁𐎟𐏐𐡗𐤟𐤿𐩐-𐩘𐩿𐬹-𐬿𑂻𑂼𑂾-𑃁𒑰-𒑳"\')>\\]}༻༽᚜⁆⁾₎〉❩❫❭❯❱❳❵⟆⟧⟩⟫⟭⟯⦄⦆⦈⦊⦌⦎⦐⦒⦔⦖⦘⧙⧛⧽⸣⸥⸧⸩〉》」』】〕〗〙〛〞〟﴿︘︶︸︺︼︾﹀﹂﹄﹈﹚﹜﹞)]}⦆」»’”›⸃⸅⸊⸍⸝⸡‛‟«‘“‹⸂⸄⸉⸌⸜⸠‚„]))', ['(?P(?:(?!_)\\w)+(?:[-._+:](?:(?!_)\\w)+)*)(?P__?)', ('footnotelabel', '\\[', '(?P\\]_)', ['[0-9]+', '\\#((?:(?!_)\\w)+(?:[-._+:](?:(?!_)\\w)+)*)?', '\\*', '(?P(?:(?!_)\\w)+(?:[-._+:](?:(?!_)\\w)+)*)'])]), ('backquote', '(?P(:(?:(?!_)\\w)+(?:[-._+:](?:(?!_)\\w)+)*:)?)', '(?!\\s)', ['`(?!`)'])]) self = settings = start_string_prefix = '(^|(?<=\\s|["\'(<\\[{༺༼᚛⁅⁽₍〈❨❪❬❮❰❲❴⟅⟦⟨⟪⟬⟮⦃⦅⦇⦉⦋⦍⦏⦑⦓⦕⦗⧘⧚⧼⸢⸤⸦⸨〈《「『【〔〖〘〚〝〝﴾︗︵︷︹︻︽︿﹁﹃﹇﹙﹛﹝([{⦅「«‘“‹⸂⸄⸉⸌⸜⸠‚„»’”›⸃⸅⸊⸍⸝⸡‛‟\\-/:֊¡·¿;·՚-՟։־׀׃׆׳״؉؊،؍؛؞؟٪-٭۔܀-܍߷-߹࠰-࠾।॥॰෴๏๚๛༄-༒྅࿐-࿔၊-၏჻፡-፨᐀᙭᙮᛫-᛭᜵᜶។-៖៘-៚᠀-᠊᥄᥅᧞᧟᨞᨟᪠-᪦᪨-᪭᭚-᭠᰻-᰿᱾᱿᳓‐-‗†-‧‰-‸※-‾⁁-⁃⁇-⁑⁓⁕-⁞⳹-⳼⳾⳿⸀⸁⸆-⸈⸋⸎-⸛⸞⸟⸪-⸮⸰⸱、-〃〜〰〽゠・꓾꓿꘍-꘏꙳꙾꛲-꛷꡴-꡷꣎꣏꣸-꣺꤮꤯꥟꧁-꧍꧞꧟꩜-꩟꫞꫟꯫︐-︖︙︰-︲﹅﹆﹉-﹌﹐-﹒﹔-﹘﹟-﹡﹣﹨﹪﹫!-#%-'*,-/:;?@\。、・𐄀𐄁𐎟𐏐𐡗𐤟𐤿𐩐-𐩘𐩿𐬹-𐬿𑂻𑂼𑂾-𑃁𒑰-𒑳]))' AttributeError: 'Values' object has no attribute 'pep_references' ```
JasonGross commented 3 years ago

@cpitclaudel do you have any idea what's going on here?

cpitclaudel commented 3 years ago

I will look soon

cpitclaudel commented 3 years ago

Quick check: which command is yielding this result? You're processing a .v file with embedded reST? Or with embedded Coqdoc?

JasonGross commented 3 years ago

I'm invoking python3 etc/alectryon/alectryon.py --frontend coq+rst --backend webpage --sertop-arg=--no_prelude --sertop-arg=--indices-matter -R "./theories" HoTT -Q "./contrib" HoTT.Contrib --output-directory alectryon-html --cache-directory alectryon-cache ./theories/Basics.v ./theories/Basics/Notations.v ./theories/Basics/Utf8.v ... with a couple hundred more .v files, it looks like it's processing theories/Basics.v. I'm claiming there's embedded reST, but in fact we haven't added any yet.

JasonGross commented 3 years ago

It looks like there was a similar issue in Sphinx (https://github.com/sphinx-doc/sphinx/pull/4512) that was fixed by

 default_settings = {
     'embed_stylesheet': False,
     'cloak_email_addresses': True,
     'pep_base_url': 'https://www.python.org/dev/peps/',
+    'pep_references': None,
     'rfc_base_url': 'https://tools.ietf.org/html/',
+    'rfc_references': None,
     'input_encoding': 'utf-8-sig',
     'doctitle_xform': False,
     'sectsubtitle_xform': False,
     'halt_level': 5,
     'file_insertion_enabled': True,
     'smartquotes_locales': [],
 }

in sphinx/environment/__init__.py

cpitclaudel commented 3 years ago

Thanks, I saw that one, but I should be inheriting all default settings in RstCoqParser:

class RSTCoqParser(docutils.parsers.rst.Parser):
    """A wrapper around the reStructuredText parser for literate Coq files."""

    supported = ('coq',)
    """Aliases this parser supports."""

    settings_spec = ('Literate Coq Parser Options', None,
                     docutils.parsers.rst.Parser.settings_spec[2]) # ← Here

Which version of docutils are you using?

cpitclaudel commented 3 years ago

it looks like it's processing theories/Basics.v. I'm claiming there's embedded reST, but in fact we haven't added any yet.

If you run that same command manually, with just theories/Basics.v, do you get the same issue?

cpitclaudel commented 3 years ago

Reproduced by upgrading to 0.17

JasonGross commented 3 years ago

That's strange, given that we seem to have succeeded on docutils-0.17 (see https://github.com/HoTT/HoTT/runs/2353352310?check_suite_focus=true), but we are failing on docutils-0.17.1. In any case, the failure occurs with docutils 0.17.1 [release] and Python version 3.7.3.

cpitclaudel commented 3 years ago

Ah sorry, I meant I updated to the latest from 0.16, and things are now reproducing; it could be that the culprit is 17.1 instead of 17. Will look right away.