Permalink
Commits on Jan 16, 2019
  1. Merge pull request #604 from Gaj7/master

    xrchz committed Jan 16, 2019
    Add header file for compcert compatibility
  2. Merge pull request #591 from CakeML/better-names

    xrchz committed Jan 16, 2019
    Better names
Commits on Jan 15, 2019
  1. Add header file for compcert compatibility

    Gaj7 committed Jan 15, 2019
  2. Update for ref --> Ref

    myreen committed Jan 15, 2019
  3. Update CF examples for True, False, Ref

    myreen committed Jan 15, 2019
Commits on Jan 14, 2019
  1. Fix typo in how-to.md

    myreen committed Jan 14, 2019
  2. Update how-to.md for change to True, False, Ref

    myreen committed Jan 14, 2019
  3. Fix source_to_flatProof for new constructor names

    xrchz committed Jan 14, 2019
  4. Merge pull request #599 from CakeML/lem-readme

    xrchz committed Jan 14, 2019
    Add lem version into semantics README
  5. Merge remote-tracking branch 'origin/master' into better-names

    xrchz committed Jan 14, 2019
    Regenerate Lem-based script files to resolve a merge conflict.
  6. Update lexer, grammar and parser to remove special treatment of "ref"

    mn200 committed Jan 13, 2019
    References in the expression language are all via the
    pseudo-constructor "Ref" and the type name "ref" is just handled as a
    normal type name. cmlPTreeConversion handles both and turns expresion
    forms into the Opref operator, and types into the special Ref type.
  7. Add lem version into semantics README

    formrre committed Jan 13, 2019
Commits on Jan 9, 2019
  1. Merge pull request #597 from CakeML/lem-194778e

    xrchz committed Jan 9, 2019
    Lem 194778e
Commits on Jan 8, 2019
  1. Remove unused lem stubs

    formrre committed Jan 8, 2019
  2. Merge pull request #595 from CakeML/local

    xrchz committed Jan 8, 2019
    Local blocks in ml_progLib
Commits on Jan 7, 2019
  1. Work around a parsing bug in HOL

    myreen committed Jan 7, 2019
Commits on Jan 4, 2019
  1. Fix manual eval_rel proof in monad translator.

    Thomas Sewell
    Thomas Sewell committed Jan 4, 2019
    Fix another instance where an 'eval_rel' goal is constructed by
    repeat manipulation of an ML_code thm (whose form has changed)
    rather than just fetching the state and env component.
    
    The monad translator seems to be working now.
Commits on Jan 3, 2019
  1. Many compatibility fiddles for ML_code changes.

    Thomas Sewell
    Thomas Sewell committed Jan 3, 2019
    Lots of adventures in hunting down slight incompatibilities between
    the translator and the basis. The basis theories now all build.
    
    In particular:
      - ensure that 'env' objects are abbreviated without being normalised.
        + the definitions of write/write_cons/merge_env etc will eventually be
          added to the global compute set.
      - ensure that auto-names of _v constants are exactly as before.
        + basisFunctionsLib.trans uses part of a _v constant name to guess
          a v_thm name and overwrite the translator thm with a rewritten version.
      - delete chunks of various scripts that reimplement parts of ml_progLib
        e.g. doing ml_progLib.get_state by hand via rator/rator/rand.
      - add some more queries to ml_progLib/ml_translatorLib to delete yet more
        hand interventions from other theories.
Commits on Dec 31, 2018
  1. Rename to lowercase code-of-conduct.md

    xrchz committed Dec 27, 2018
  2. Add CODE_OF_CONDUCT.md

    xrchz committed Dec 27, 2018
Commits on Dec 30, 2018
  1. Bugfix in EVAL setup in ml_progLib changes.

    Thomas Sewell
    Thomas Sewell committed Dec 30, 2018
    The v_thms were being constructed with the wrong flag and added to
    the EVAL/computeLib set.
  2. Permit nested modules in ml_translator.

    Thomas Sewell
    Thomas Sewell committed Dec 30, 2018
    The ml_translator code can now compute long names of arbitrary length,
    permitting the use of constants/types/etc defined in nested modules.
    This is tested in at least one simple case.
  3. Support for local blocks in ml_progLib.

    Thomas Sewell
    Thomas Sewell committed Dec 30, 2018
    Adds a new interface to ml_progLib for progressively defining a
    'local .. in .. end' block via open_local_block, open_local_in_block
    and then close_local_block.
  4. Tweak alist_treeLib again.

    Thomas Sewell
    Thomas Sewell committed Dec 30, 2018
    Fix a bug and generally refactor the bit about representing terms
    which are merges/option-choices of terms with existing representations.
  5. Remove unused parsing gitignore

    xrchz committed Dec 30, 2018
  6. Merge pull request #590 from CakeML/howto

    xrchz committed Dec 30, 2018
    Add a how-to file explaining how to use the compiler
  7. Missed some commas

    xrchz committed Dec 30, 2018
  8. Rename 'input' to 'test-hello'

    xrchz committed Dec 30, 2018
  9. Make a few tweaks to how-to.md

    xrchz committed Dec 30, 2018
Commits on Dec 29, 2018
  1. Typo in how-to.md

    myreen committed Dec 29, 2018