Serapi perhaps giving a strange human string of proof states after induction?

[brando90]

From the example on the docs the format of the proof state should be something like:

              ((CoqString  "\
                          \n  local context\
                          \n============================\
                          \ngoals...

but in induction the goals are interleaved randomly with the local context:

(Answer 2
 (ObjList
  ((CoqString
     "none\
    \n============================\
    \n0 + 0 = 0\
    \n\
    \n  IH : n' + 0 = n'\
    \n  n' : nat\
    \n============================\
    \nS n' + 0 = S n'"))))
(Answer 2 Completed)

is this a bug?

---

whole exchange:

(Add () "
Theorem add_easy_induct_1:
forall n:nat,
  n + 0 = n.
Proof.
  intros.
  induction n as [| n' IH].
")
(Answer 0 Ack)
(Answer 0
 (Added 2
  ((fname ToplevelInput) (line_nb 2) (bol_pos 1) (line_nb_last 4)
   (bol_pos_last 42) (bp 1) (ep 54))
  NewTip))
(Answer 0
 (Added 3
  ((fname ToplevelInput) (line_nb 5) (bol_pos 55) (line_nb_last 5)
   (bol_pos_last 55) (bp 55) (ep 61))
  NewTip))
(Answer 0
 (Added 4
  ((fname ToplevelInput) (line_nb 6) (bol_pos 62) (line_nb_last 6)
   (bol_pos_last 62) (bp 64) (ep 71))
  NewTip))
(Answer 0
 (Added 5
  ((fname ToplevelInput) (line_nb 7) (bol_pos 72) (line_nb_last 7)
   (bol_pos_last 72) (bp 74) (ep 99))
  NewTip))
(Answer 0 Completed)

(Exec 5)
(Answer 1 Ack)
(Feedback
 ((doc_id 0) (span_id 5) (route 0) (contents (ProcessingIn master))))
(Feedback
 ((doc_id 0) (span_id 4) (route 0) (contents (ProcessingIn master))))
(Feedback
 ((doc_id 0) (span_id 3) (route 0) (contents (ProcessingIn master))))
(Feedback
 ((doc_id 0) (span_id 2) (route 0) (contents (ProcessingIn master))))
(Feedback ((doc_id 0) (span_id 1) (route 0) (contents Processed)))
(Feedback ((doc_id 0) (span_id 2) (route 0) (contents Processed)))
(Feedback ((doc_id 0) (span_id 3) (route 0) (contents Processed)))
(Feedback ((doc_id 0) (span_id 4) (route 0) (contents Processed)))
(Feedback ((doc_id 0) (span_id 5) (route 0) (contents Processed)))
(Answer 1 Completed)

(Query ((pp ((pp_format PpStr)))) Goals)
(Answer 2 Ack)
(Answer 2
 (ObjList
  ((CoqString
     "none\
    \n============================\
    \n0 + 0 = 0\
    \n\
    \n  IH : n' + 0 = n'\
    \n  n' : nat\
    \n============================\
    \nS n' + 0 = S n'"))))
(Answer 2 Completed)

[brando90]

commands:

rlwrap sertop --printer=human

(Add () "
Theorem add_easy_induct_1:
forall n:nat,
  n + 0 = n.
Proof.
  intros.
  induction n as [| n' IH].
")
(Exec 5)
(Query ((pp ((pp_format PpStr)))) Goals)

[brando90]

note the display in jscoq, doesn't have the goals randomly interleaved with the local context:

2 goals

0 + 0 = 0
2
S n' + 0 = S n'

what I want after that command is to see the local context and all the goals seperately.

[ejgallego]

What's strange about the response? Ut is just printing the goals sequentially, there are not randomly interleaved, I see they are normal, first goal 0 = 0 (no hyps) second goal the inductive case with their corresponding hyps.

If you need finer goal manipulation you want to first access the goal representation and call the printer as you want.

[ejgallego]

I don't understand the problem, feel free to provide more info, cheers.