compilation problems in CI with Coq 8.20 (dev)

[rmatthes]

As mentioned in PR #1829, there are now errors when compiling with the Coq development version. The two errors on display are in the files

• UniMath/Bicategories/DisplayedBicats/Examples/Codomain.v
• UniMath/Bicategories/OrthogonalFactorization/EsoFactorizationSystem.v
  Both errors concern unification (one in the form of matching).
  I did not look into that problem. It would be good to find out if this is a regression to be reported to the Coq developers (I am not sure that they compile the bicategories package) or if it has an easy fix.

EDIT by @benediktahrens :
One compile error is visible here: https://github.com/UniMath/UniMath/actions/runs/7713706867/job/21024231409. It reads as

  File "./UniMath/Bicategories/DisplayedBicats/Examples/Codomain.v", line 665, characters 11-56:
  Error:
  Found no subterm matching "pr1
                               (transportf (λ x : ?A, ∑ b : ?B x, ?P x b) 
                                  ?M33 ?M34)" in p.
  
          coqc UniMath/Bicategories/OrthogonalFactorization/EsoFactorizationSystem.{glob,vo} (exit 1)
  File "./UniMath/Bicategories/OrthogonalFactorization/EsoFactorizationSystem.v", line 66, characters 10-12:
  Error:
  In environment
  B : bicat
  fact_B : eso_ff_factorization B
  HB_2_1 : is_univalent_2_1 B
  b₁, b₂, c₁, c₂ : B
  e : B ⟦ b₁, b₂ ⟧
  m : B ⟦ c₁, c₂ ⟧
  He : is_eso e,,
       eso_ff_orthogonal_factorization_system_subproof B HB_2_1 b₁ b₂ e
  Hm : fully_faithful_1cell m,,
       eso_ff_orthogonal_factorization_system_subproof0 B c₁ c₂ m
  Unable to unify
   "hProptoType
      (is_eso e,,
       eso_ff_orthogonal_factorization_system_subproof B HB_2_1 b₁ b₂ e)" with
   "e ⊥ m".

[nmvdw]

They do not compile the bicategories package due to memory consumption (so, I dunno whether they can pay much attention to it). My guess that in both cases the error is related to unification (for EsoFactorizationSystem.v, the relevant line uses apply and for Codomain.v, the relevant line uses rewrite). Fixing both errors is going to be easy, as it is probably only a matter of supplying more arguments.

There are 2 possible solutions:

• Change the files now by giving them more arguments. Since I do not use the development version of Coq, this might become a bit of a messy process (but it might not be too bad).
• Wait until the next version of Coq comes out, and fix the errors if the issue is still there. If we do this, then it might be best to only compile Coq dev with the sanity checks on all packages that do not use bicategories.

[benediktahrens]

It could be worth opening an issue with Coq, as soon as possible. Possibly this regression could be fixed before 8.20 is released.