Process completed with exit code 2.

Process completed with exit code 2.

Process completed with exit code 1.

pkgconf 2.3.0_1 is already installed, it's just not linked. To link this version, run: brew link pkgconf

Could not find a terminator for 6-line warning: File "./src/Coqprime/List/Permutation.v", line 97, characters 0-4: Warning: permutation_one_inv_aux is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 6-line warning: File "./src/Coqprime/List/Permutation.v", line 234, characters 0-4: Warning: permutation_cons_ex_aux is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 7-line warning: File "./src/Coqprime/List/Permutation.v", line 363, characters 0-4: Warning: all_permutations_aux_permutation is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 7-line warning: File "./src/Coqprime/List/Permutation.v", line 401, characters 0-4: Warning: permutation_all_permutations_aux is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 3-line warning: File "./src/coqutil/Semantics/OmniSmallstepCombinators.v", line 88, characters 2-139: Warning: Q cannot be defined because it is informative and always' is not. [cannot-define-projection,records,default]

Could not find a terminator for 6-line warning: File "./src/coqutil/Word/Properties.v", line 61, characters 63-67: Warning: width_nonneg_context is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 6-line warning: File "./src/coqutil/Word/Properties.v", line 228, characters 52-56: Warning: width_nonzero is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 6-line warning: File "./src/coqutil/Word/Properties.v", line 232, characters 70-74: Warning: twice_halfm is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 4-line warning: File "./src/coqutil/Tactics/SafeSimpl.v", line 19, characters 0-52: Warning: This inductive will be minimized to Set even though Universe Minimization ToSet is unset. This will change in a future version. [bad-set-minimization,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 3-line warning: File "./src/coqutil/Map/SeparationLogic.v", line 212, characters 27-64: Warning: Notation "_ ++ _" was already used in scope list_scope. [notation-overridden,parsing,default]

Could not find a terminator for 6-line warning: File "./src/Coqprime/List/Permutation.v", line 97, characters 0-4: Warning: permutation_one_inv_aux is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 6-line warning: File "./src/Coqprime/List/Permutation.v", line 234, characters 0-4: Warning: permutation_cons_ex_aux is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 7-line warning: File "./src/Coqprime/List/Permutation.v", line 363, characters 0-4: Warning: all_permutations_aux_permutation is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 7-line warning: File "./src/Coqprime/List/Permutation.v", line 401, characters 0-4: Warning: permutation_all_permutations_aux is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 3-line warning: File "./src/coqutil/Semantics/OmniSmallstepCombinators.v", line 88, characters 2-139: Warning: Q cannot be defined because it is informative and always' is not. [cannot-define-projection,records,default]

Could not find a terminator for 6-line warning: File "./src/coqutil/Word/Properties.v", line 61, characters 63-67: Warning: width_nonneg_context is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 6-line warning: File "./src/coqutil/Word/Properties.v", line 228, characters 52-56: Warning: width_nonzero is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 6-line warning: File "./src/coqutil/Word/Properties.v", line 232, characters 70-74: Warning: twice_halfm is declared opaque (Qed) but this is not fully respected inside the section and not at all outside the section. Use attribute #[clearbody] to get the current behaviour of clearing the body at the start of proofs in a forward compatible way. [opaque-let,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 4-line warning: File "./src/coqutil/Tactics/SafeSimpl.v", line 19, characters 0-52: Warning: This inductive will be minimized to Set even though Universe Minimization ToSet is unset. This will change in a future version. [bad-set-minimization,deprecated-since-8.18,deprecated,default]

Could not find a terminator for 4-line warning: File "./src/coqutil/Datatypes/OperatorOverloading.v", line 502, characters 4-48: Warning: This inductive will be minimized to Set even though Universe Minimization ToSet is unset. This will change in a future version. [bad-set-minimization,deprecated-since-8.18,deprecated,default]