search

anoma / juvix

A language for intent-centric and declarative decentralised applications
https://docs.juvix.org
GNU General Public License v3.0
449 stars 54 forks source link

Isabelle/HOL translation: recursive translation of the whole project #2977

Open lukaszcz opened 1 month ago

lukaszcz commented 1 month ago

Checklist

lukaszcz commented 4 weeks ago

The CI fails because of a bug in GHC:

[560 of 675] Compiling Juvix.Compiler.Backend.Isabelle.Translation.FromTyped

  <no location info>: error:
      panic! (the 'impossible' happened)
    GHC version 9.8.2:
    lookupIdSubst
    $sgoExpression_sBxI4
    InScope {eta_B0 eta_B1 eta_B2 wild_X2 wild_X3 eta2_XE eta3_XF
             wild_XI wild_XJ wild_XL wild_XM wild_XN wild_XO go3_anFo
             $cfmap_aB3Vz $c<$_aB3VO cl_aB45G cls_aB45J p_aB45K pat_aB45T
             $d(%,%)_aB6o2 $d(%,%)_aB6o4 $d(%,%)_aB6o7 $d(%,%)_aB6of $krep_aB6qK
             $krep_aB6qL $krep_aB6qM $krep_aB6qN $krep_aB6qO $krep_aB6qP
             $krep_aB6qQ $krep_aB6qR $krep_aB6qS $krep_aB6qT $krep_aB6qU
             $krep_aB6qV $krep_aB6qW $krep_aB6qX $krep_aB6qY $krep_aB6qZ
             $krep_aB6r0 ds_dB8SV ds_dB8VC ds_dB8VZ ds_dB8W4 ds_dB8W5 wild_iklsw
             x1_iklsx x2_iklsy wild_iBak0 x2_iBak1 x3_iBak2 x4_iBak3 x5_iBak4
             x6_iBak5 x7_iBak6 x8_iBak7 x9_iBak8 x10_iBak9 x11_iBaka x12_iBakb
             x13_iBakc _nameMap _nameSet $tc'NameSet $tcNameSet $tc'NameMap
             $tcNameMap nameSet _nestedPatterns _nestedElem nameMap $tc'Nested
             $tcNested $fFunctorNested nestedElem nestedPatterns fromInternal
             goModule $trModule $trModule_sB9Vi $trModule_sB9Vk $krep_sB9Vl
             $krep_sB9Vm $krep_sB9Vn $tcNameSet_sB9Vp $tcNameSet_sB9Vq
             $tc'NameSet_sB9Vr $tc'NameSet_sB9Vs $tcNameMap_sB9Vt
             $tcNameMap_sB9Vu $tc'NameMap_sB9Vv $tc'NameMap_sB9Vw
             $tcNested_sB9Vx $tcNested_sB9Vy $krep_sB9Vz $krep_sB9VA $krep_sB9VB
             $krep_sB9VC $krep_sB9VD $tc'Nested_sB9VE $tc'Nested_sB9VF loc_sBa04
             loc_sBa05 loc_sBa06 $dIP_sBa08 $dIP_sBa09 loc_sBa0f $dIP_sBa0q
             $dIP_sBa0s loc_sBa10 $dIP_sBa12 $dIP_sBa13 $dIP_sBa16 loc_sBa1w
             loc_sBa1O $dIP_sBa1R $dIP_sBa1S $dIP_sBa1V fromInternal_sBcsZ
             $sinsert'_sBglX $sinsert'_sBglZ $s$winsert'_sBgmL $s$winsert'_sBgnf
             $s$wupdateOrSnocWithKey_sBgnn $slookup#_sBgnz $slookup#_sBgnO
             $shash_sBgnR $shash_sBgnT $sppTrace_sBgnY $sdoc_sBgo4 poly_f_sBgpe
             lvl_sBgpf lvl_sBgHJ poly_go1_sBgK3 poly_go1_sBgKz lvl_sBgNN
             lvl_sBgNO lvl_sBgNQ lvl_sBgNR reservedNames_sBgVC
             getPatternArgName_sBgVK goRecordFields_sBgVO
             goInductiveParameter_sBgW7 mkExprCase_sBgW9 lvl_sBgWc lvl_sBgWd
             lvl_sBgWe lvl_sBgWo toIsabelleTheoryName_sBgWu lvl_sBgWA lvl_sBgWS
             c_sBgYq go1_sBgYA go1_sBgYO go1_sBgZ6 go1_sBgZo lvl_sBgZG lvl_sBgZQ
             lvl_sBh05 quoteName_sBh12 loc_sBh1i loc_sBh1k loc_sBh1m $dIP_sBh1s
             $dIP_sBh1u unsupportedType_sBh1A lvl_sBh1E lvl_sBh1F lvl_sBh1J
             txt_sBh2M txt_sBh2X txt_sBh37 txt_sBh3i txt_sBh3F lvl_sBh3G
             loc_sBh3W loc_sBh3Y loc_sBh40 $dIP_sBh46 $dIP_sBh48 lvl_sBh49
             loc_sBh4S loc_sBh4U $dIP_sBh50 $dIP_sBh52 $dIP_sBh54 lvl_sBh5A
             lvl_sBh5B lvl_sBhda lvl_sBhez lvl_sBheA lvl_sBheB lvl_sBheC
             lvl_sBheF lvl_sBhf1 loc_sBhgk loc_sBhgm loc_sBhgt $dIP_sBhhL
             $dIP_sBhhR loc_sBhi9 loc_sBhie loc_sBhig $dIP_sBhik $dIP_sBhim
             $dIP_sBhio loc_sBhjM loc_sBhjO loc_sBhjQ $dIP_sBhjU $dIP_sBhk1
             $dIP_sBhk7 lvl_sBhmP lvl_sBhnD lvl_sBhoj lvl_sBhql lvl_sBhqm
             n_sBhzC n_sBhzN lvl_sBhA2 lvl_sBhAy lvl_sBhAG lvl_sBhAI lvl_sBhEi
             lvl_sBhEF lvl_sBhEH lvl_sBhEI lvl_sBhF7 lvl_sBhFH lvl_sBhFM n_sBhHV
             lvl_sBhIG lvl_sBhIM lvl_sBhIO lvl_sBhIP ds_sBhJ7 lvl_sBhJ9
             lvl_sBhJR lvl_sBhK4 lvl_sBhKi lvl_sBhKj lvl_sBhKv lvl_sBhKD
             lvl_sBhLa lvl_sBhMi $dIP_sBnQ3 $dIP_sBnQ8 $dIP_sBnQp $dIP_sBnR5
             $dIP_sBnRs $w$j2_sBrdt $wgoNestedBranches_sBreh $wunsafeDrop_sBreI
             $wfilterTypeArgs_sBrf5 $w$j2_sBrfP $wpoly_go2_sBrh6
             $wpoly_go1_sBrhr $wpoly_go2_sBri2 $wpoly_go1_sBrin
             $wlocalName_sBriJ $wpoly_go2_sBrj6 $wpoly_go1_sBrjq $wquote'_sBrjO
             $wtoIsabelleTheoryName_sBrlh $wquote_sBro6 $wquoteName_sBrtd
             $wpoly_go1_sBrwo $wlookupName_sBrxY $wlvl_sBrza ww_sBrBJ ww_sBrBK
             ww_sBrBL ww_sBrBQ onlyTypes_sBrGz infoTable_sBrGA ww_sBrGE ww_sBrGF
             ww_sBrGG $wgoModule_sBrGK $wfromInternal_sBrHo ww_sBrI1 ww_sBrI2
             ww_sBrI3 lvl_sBtCb lvl_sBtCc lvl_sBtCd lvl_sBtCe lvl_sBtCf
             lvl_sBtCg lvl_sBtCh lvl_sBtCi lvl_sBtCj lvl_sBtCk lvl_sBtCm
             lvl_sBtCn lvl_sBtCo lvl_sBtCp lvl_sBtCq lvl_sBtCr lvl_sBtCy
             lvl_sBtCz lvl_sBtCB lvl_sBtCC lvl_sBtCD lvl_sBtCE lvl_sBtCF
             lvl_sBtCM lvl_sBtCN lvl_sBtCP lvl_sBtCQ lvl_sBtCR lvl_sBtD0
             lvl_sBtD1 lvl_sBtD3 lvl_sBtD4 lvl_sBtD5 lvl_sBtDe lvl_sBtDf
             lvl_sBtDh lvl_sBtDi lvl_sBtDj lvl_sBtDs lvl_sBtDt lvl_sBtDw
             lvl_sBtDx lvl_sBtDy lvl_sBtDH lvl_sBtDI lvl_sBtDK lvl_sBtDL
             lvl_sBtDM lvl_sBtDN lvl_sBtDX lvl_sBtEa lvl_sBtEd lvl_sBtEe
             lvl_sBtEf lvl_sBtEo lvl_sBtEp lvl_sBtEs lvl_sBtEt lvl_sBtEu
             lvl_sBtED lvl_sBtEE lvl_sBtEG lvl_sBtEH lvl_sBtEI lvl_sBtEJ
             lvl_sBtEK lvl_sBtEL lvl_sBtEM lvl_sBtET lvl_sBtEU lvl_sBtEW
             lvl_sBtEX lvl_sBtEY lvl_sBtEZ lvl_sBtF0 lvl_sBtF9 lvl_sBtFc
             lvl_sBtFd lvl_sBtFe lvl_sBtFn lvl_sBtFr lvl_sBtFs lvl_sBtFv
             lvl_sBtFw lvl_sBtFD lvl_sBtFH lvl_sBtFI lvl_sBtFJ lvl_sBtFK
             lvl_sBtFL lvl_sBtFM lvl_sBtFN lvl_sBtFP lvl_sBtFQ lvl_sBtFS
             lvl_sBtFT lvl_sBtFU lvl_sBtFW lvl_sBtFX lvl_sBtFY lvl_sBtFZ
             lvl_sBtG0 lvl_sBtG1 lvl_sBtG2 lvl_sBtG3 lvl_sBtG4 lvl_sBtG8
             lvl_sBtG9 lvl_sBtGa lvl_sBtGh lvl_sBtGk lvl_sBtGl lvl_sBtGm
             lvl_sBtGn lvl_sBtGu lvl_sBtGv lvl_sBtGx lvl_sBtGy lvl_sBtGz
             lvl_sBtGA lvl_sBtGB lvl_sBtGG lvl_sBtGI lvl_sBtGL lvl_sBtGZ
             lvl_sBtH3 lvl_sBtH4 lvl_sBtHd lvl_sBtHh lvl_sBtHi go1_sBtHk
             go1_sBtHm xs_sBtHq go1_sBtHs poly_go_sBtHu lvl_sBtMB lvl_sBtMI
             lvl_sBtMK lvl_sBtMM lvl_sBtMO lvl_sBu1Z lvl_sBu2h lvl_sBu2J
             lvl_sBu37 lvl_sBu3u lvl_sBu3Q lvl_sBu4i lvl_sBu4I lvl_sBu54
             lvl_sBu5t lvl_sBu5P lvl_sBu6g lvl_sBu6E lvl_sBu7b lvl_sBu7D
             lvl_sBu8a lvl_sBu8B lvl_sBu91 $j_sBujL $j_sBujN lvl_sBujO lvl_sBujP
             lvl_sBujQ lvl_sBuk0 lvl_sBuk1 lvl_sBuk4 lvl_sBuk5 lvl_sBuk8
             lvl_sBul3 lvl_sBul7 lvl_sBul8 $j_sBulc lvl_sBule lvl_sBulx
             lvl_sBulM lvl_sBulN lvl_sBulO lvl_sBulP lvl_sBulU lvl_sBulV
             lvl_sBulW lvl_sBulX lvl_sBuqd lvl_sBuqg go1_sBurl go1_sBurt
             go1_sButz sc_sBxI1 sg_sBxI2 sg_sBxKz $sgo1_sBye2 $s$wpoly_go1_sByjA
             $s$wpoly_go2_sBykb $s$wpoly_go2_sBymZ $s$wpoly_go2_sByn0
             $s$wgo2_sByq6 $s$wgo2_sByqf $s$wgo2_sByqw $s$wgo2_sByqP
             $s$wgo2_sByqY $s$wgo2_sByrf $s$wgo2_sByry $s$wgo2_sByrH
             $s$wgo2_sByrY $s$wgo2_sBysh $s$wgo2_sBysq $s$wgo2_sBysH
             $s$wpoly_go1_sByHg $s$wpoly_go1_sByRu $s$wpoly_go1_sBySd
             $sgoRecordFields_sByTj $s$wgoNestedBranches'_sByTu $sgo1_sByTB
             lvl_sBz0D lvl_sBz0F mkIndType_sBz0H goType_sBz0J
             goRecordField_sBz0P lvl_sBz0R goConstructorDef_sBz0T lvl_sBz0V
             getList_sBz0X lvl_sBz0Z $wgetListPat_sBz11 names_sBz13
             disambiguate_sBz1e $wgoConstrName_sBz1g goPatternArgs_sBz1i
             $wgoNestedPattern_sBz1l goPatternArg_sBz1m $sgoPatternArg_sBz1n
             $wgoPatternArgCase_sBz6o $sgoExpression_sBz6q
             $sgoLambdaClauses_sBz6s $sgoExpression_sBz6t
             $sgoLambdaClauses_sBz6u goLambdaClauses_sBz6v goExpression_sBz6w
             $sgoLambdaClauses_sBz6x $sgoExpression_sBz6y sc_sBzm7 sc_sBzm8}
    Call stack:
        CallStack (from HasCallStack):
          callStackDoc, called at compiler/GHC/Utils/Panic.hs:191:37 in ghc-9.8.2-2c96:GHC.Utils.Panic
          pprPanic, called at compiler/GHC/Core/Subst.hs:197:17 in ghc-9.8.2-2c96:GHC.Core.Subst
    CallStack (from HasCallStack):
      panic, called at compiler/GHC/Utils/Error.hs:503:29 in ghc-9.8.2-2c96:GHC.Utils.Error

  Please report this as a GHC bug:  https://www.haskell.org/ghc/reportabug

The problem is with one of the optimizations (it works with optimizations turned off).

Possibly related:

paulcadman commented 1 week ago

This PR is blocked until we can solve:

Which probably means we need to wait for stackage nightly to update to GHC 9.10.1.