Universe Inconsistencies
Closed this issue · 3 comments
mrhaandi commented
To be prepared for future universe inconsistencies, I tried to Require all _undec files.
This did produce current universe inconsistencies which I do not understand.
From Undecidability Require
TM.SBTM_undec TM.TM_undec
SystemF.SysF_undec
StringRewriting.PCSnf_undec StringRewriting.SR_undec StringRewriting.SSTS_undec
StackMachines.BSM_undec StackMachines.SMN_undec StackMachines.SSM_undec
SOL.PA2_undec SOL.SOL_undec
SetConstraints.FMsetC_undec
SeparationLogic.MSL_undec SeparationLogic.SL_undec
SemiUnification.SemiU_undec PolynomialConstraints.LPolyNC_undec
PCP.PCP_undec
MuRec.MuRec_undec
MinskyMachines.MM_undec MinskyMachines.MM2_undec MinskyMachines.MMA2_undec MinskyMachines.ndMM2_undec
LambdaCalculus.Krivine_undec LambdaCalculus.wCBN_undec
L.L_undec
ILL.CLL_undec ILL.ILL_undec ILL.IMSELL_undec
HilbertCalculi.HSC_undec
H10.H10_undec H10.H10p_undec H10.H10Z_undec
FRACTRAN.FRACTRAN_undec
FOL.binFOL_undec FOL.binZF_undec FOL.FOL_undec FOL.FSAT_undec FOL.minFOL_undec FOL.minZF_undec FOL.PA_undec FOL.ZF_undec
DiophantineConstraints.H10C_undec
CounterMachines.CM1_undec CounterMachines.CM2_undec
CFG.CFG_undec CFG.CFP_undec.For reference, the current error message is
Universe inconsistency. Cannot enforce EqDecDef.eqType.u0 < list.u0 because
list.u0 = EqDecDef.eqType.u0.
The above only includes _undec.v files. Since it is already inconsistent, I did not manually included HOU, TRAKHTENBROT, or other ad-hoc results.
yforster commented
Can you for reference post the error message?
One we have resolved the problem we could in principle require such a global test file for the CI