Dissapearing goal

[vzaliva]

Stepping through the proof after some tactics, *goals* window is empty. Neither C-c C-p nor C-c C-l help.

Version: 20200623.1748 from MELPA. This is very critical. PG is not usable until this fixed. There is no known workaround.

[vzaliva]

Maybe this will help. Last message from *coq* buffer after which the goal disappears. Maybe there is a problem parsing it?

<prompt>memory_invariant_after_init < 463 |memory_invariant_after_init| 0 < </prompt>repeat break_match_hyp; try inl_inr;     inv LI ; repeat inv_sum;  inv Heqs4.
1 subgoal (ID 8895)

  data, hdata : list binary64
  i, o : Int64.int
  name : string
  globals : list (string * DSHType)
  op : DSHOperator
  l : list binary64
  m : mem_block
  Co : constMemBlock (MInt64asNT.to_nat o) data ≡ (l, m)
  l0 : list binary64
  m0 : mem_block
  Ci : constMemBlock (MInt64asNT.to_nat i) l ≡ (l0, m0)
  e : evalContext
  mg : memoryH
  G : initFSHGlobals l0 helix_empty_memory globals ≡ inr (mg, hdata, e)
  i0 : IRState
  l1 : list binary64
  t : toplevel_entities typ (LLVMAst.block typ * list (LLVMAst.block typ))
  Heqs0 : initXYplaceholders i o data (Anon 0%Z)
            (TYPE_Array (Int64.intval i) TYPE_Double) 
            (Anon 1%Z) (TYPE_Array (Int64.intval o) TYPE_Double) newState
          ≡ inr (i0, (l1, t))
  i1 : IRState
  l2 : list binary64
  l3 : list
         (toplevel_entity typ (LLVMAst.block typ * list (LLVMAst.block typ)))
  Heqs1 : initIRGlobals l1 globals
            {|
            block_count := block_count i0;
            local_count := local_count i0;
            void_count := void_count i0;
            Γ := (ID_Local (Name "Y"),
                 TYPE_Pointer (TYPE_Array (Int64.intval o) TYPE_Double))
                 :: (ID_Local (Name "X"),
                    TYPE_Pointer (TYPE_Array (Int64.intval i) TYPE_Double))
                    :: Γ i0 |} ≡ inr (i1, (l2, l3))
  i5 : IRState
  b : block_id
  l9 : list (LLVMAst.block typ)
  Heqs6 : genIR op (Name (String "b" (string_of_nat (block_count i1))))
            {|
            block_count := S (S (block_count i1));
            local_count := local_count i1;
            void_count := void_count i1;
            Γ := Γ i1 |} ≡ inr (i5, (b, l9))
  p10 : LLVMAst.block typ * list (LLVMAst.block typ)
  i4 : IRState
  Heqs8 : body_non_empty_cast
            (l9 ++
             [{|
              blk_id := Name (String "b" (string_of_nat (block_count i1)));
              blk_phis := [ ];
              blk_code := [ ];
              blk_term := (IId
                             (Name
                                (String "b"
                                   (string_of_nat (S (block_count i1))))),
                          TERM_Ret_void);
              blk_comments := None |}]) i5 ≡ inr (i4, p10)
  l5 : list (ident * typ)
  p6, p7 : ident * typ
  Heql7 : Γ i4 ≡ p6 :: p7 :: l5
  ============================
  eutt
    (λ '(memH, _) '(memV, (l4, _, (g, _))),
       state_invariant
         (e ++
          [DSHPtrVal (S (Datatypes.length globals)) o;
          DSHPtrVal (Datatypes.length globals) i])
         {|
         block_count := block_count i4;
         local_count := local_count i4;
         void_count := void_count i4;
         Γ := l5 |} memH (memV, (l4, g)))
    (Ret
       (memory_set (memory_set mg (S (Datatypes.length globals)) m)
          (Datatypes.length globals) m0, ()))
    (with_err_LT
       (interp_mcfg
          (build_global_environment
             (mcfg_of_tle
                (l3 ++
                 t ++
                 [TLE_Comment "Prototypes for intrinsics we use";
                 TLE_Declaration maxnum_32_decl;
                 TLE_Declaration maxnum_64_decl;
                 TLE_Declaration minimum_64_decl;
                 TLE_Declaration IntrinsicsDefinitions.fabs_32_decl;
                 TLE_Declaration IntrinsicsDefinitions.fabs_64_decl;
                 TLE_Declaration IntrinsicsDefinitions.memcpy_8_decl;
                 TLE_Comment "Top-level operator definition";
                 TLE_Definition
                   {|
                   df_prototype := {|
                                   dc_name := Name name;
                                   dc_type := TYPE_Function TYPE_Void
                                                [TYPE_Pointer
                                                   (TYPE_Array 
                                                   (Int64.intval i) TYPE_Double);
                                                TYPE_Pointer
                                                  (TYPE_Array 
                                                   (Int64.intval o) TYPE_Double)];
                                   dc_param_attrs := ([ ],
                                                   [
                                                   PARAMATTR_Readonly
                                                   :: ArrayPtrParamAttrs;
                                                   ArrayPtrParamAttrs]);
                                   dc_linkage := None;
                                   dc_visibility := None;
                                   dc_dll_storage := None;
                                   dc_cconv := None;
                                   dc_attrs := [ ];
                                   dc_section := None;
                                   dc_align := None;
                                   dc_gc := None |};
                   df_args := [Name "X"; Name "Y"];
                   df_instrs := p10 |}] ++
                 genMain name (Anon 0%Z)
                   (TYPE_Pointer (TYPE_Array (Int64.intval i) TYPE_Double))
                   (Anon 1%Z) (TYPE_Array (Int64.intval o) TYPE_Double)
                   (TYPE_Pointer (TYPE_Array (Int64.intval o) TYPE_Double)))))
          [ ] ([ ], [ ]) empty_memory_stack))

<prompt>memory_invariant_after_init < 464 |memory_invariant_after_init| 0 < </prompt>

[cpitclaudel]

This is very critical. PG is not usable until this fixed. There is no known workaround.

Indeed, it sounds pretty bad — can you have a look at which commit introduced the issue? Or is it with a new Coq version?

[vzaliva]

I've restarted emacs and it helped. I do not know how I get my PG in such state. Re-opening files or stopping Coq process did not help. Let me test this a bit more and if it does not re-appear I will close this issue.

[vzaliva]

back to normal it seems. sorry for false alert.