1. 09 May, 2019 1 commit
    • Sylvain Dailler's avatar
      [WIP] This is ongoing experimental work. · 035a91c6
      Sylvain Dailler authored
      Change the way shapes are saved. The shape files is now organized as
      - first, the shapes of all declarations that were converted to shape
      - second, checksum followed by a string representing the succession of
      variables declarations.
      "(* Recording of all shape variable declarations *)
      left case
      right case
      (* Checksum then concatenated variables representing a task shape *)
      956169bfb451ee6459ffdc4df18de7fd H3H2H3
      4dceea9c71fce658291b3212396973a6 H1H2H3
      566331d4fbc568133c5beace068734c6 H0H1H2H1
      bf3e0320b4b7af8d182c9aaa24ff2ee7 H5H2H3
      03fe7b1734fc43b78ef069c15b8ceef0 H4H5H2H5
      Other changes:
      - Transform to shape only the local declarations
      - The shape size limit is now per declarations
      - It seems to reduce the size of the shapes a little
      - We read the session Xml twice just to be able to get the version of the
      shape before reading them
      - Data structure to record correspondence between shape and variable index
      seems inefficient (GShape)
      - At saving, the shapes need to be recomputed in order to not save useless
      shape variables (or temporary goals that were removed). This does not seem
      to be too inefficient: To be decided.
      - shapes should now be saved as a list of integer instead of strings
      - Pairing is under change. Proposed measure during brainstorming with
      Claude -> lcp measure replaced by the lexicographic order on:
      (number of same hypotheses, lcp on explanations, lcp on goal shape)
      - hyp_sep is "H". To be decided
      - all remaining TODO in the code
  2. 07 May, 2019 1 commit
  3. 06 May, 2019 1 commit
  4. 02 May, 2019 1 commit
  5. 30 Apr, 2019 5 commits
  6. 29 Apr, 2019 1 commit
  7. 26 Apr, 2019 2 commits
    • Sylvain Dailler's avatar
      Merge branch 'issue_17' · 79774910
      Sylvain Dailler authored
      fix #17
    • Sylvain Dailler's avatar
      Fix popups of bisect/remove · ad5327d1
      Sylvain Dailler authored
      Rewriting of remove using d_syms/d_news.
      The popup should not appear anymore as the corresponding fatal exception
      is now matched inside remove.
      The new exception raised by remove is not fatal. And, the associated
      message should overall be better.
  8. 25 Apr, 2019 12 commits
  9. 24 Apr, 2019 3 commits
  10. 23 Apr, 2019 3 commits
  11. 19 Apr, 2019 6 commits
  12. 17 Apr, 2019 3 commits
  13. 16 Apr, 2019 1 commit