Code

Faster#7

Code

Merged

benjub merged 52 commits intodavid-a-wheeler:masterdavid-a-wheeler/mmverify.py:masterfrom benjub:fasterbenjub/mmverify.py:fasterCopy head branch name to clipboardMay 6, 2022

+537-293

Commits

Commits on Mar 30, 2022

• code formatting (autopep)

  benjub

  committed
  caa3ac0

  Copy full SHA for caa3ac0

• autopep8 --aggressive --aggressive

  benjub

  committed
  249282b

  Copy full SHA for 249282b

• remove three unused variables and two superfluous 'reversed'

  benjub

  committed
  3e59796

  Copy full SHA for 3e59796

• streamline function 'readc'

  benjub

  committed
  f1bf63f

  Copy full SHA for f1bf63f

• two comment typos

  benjub

  committed
  546a092

  Copy full SHA for 546a092

• variable name consistency; logging message consistency

  benjub

  committed
  b461763

  Copy full SHA for b461763

• avoid duplicate fetching

  benjub

  committed
  92fbdc9

  Copy full SHA for 92fbdc9

• fix bug when begin_label is an -statement

  benjub

  committed
  491e277

  Copy full SHA for 491e277

• apply_subst is not a method

  benjub

  committed
  889209c

  Copy full SHA for 889209c

• refactor to avoid superfluous calls to make_assertion by decompress_proof

  benjub

  committed
  5d3c722

  Copy full SHA for 5d3c722

• add function equal_subst; upgrade code from the deprecated optparse to argparse

  benjub

  committed
  562f671

  Copy full SHA for 562f671

Commits on Mar 31, 2022

• add command arguments: optional verbosity level, and file to verify (default=stdin)

  benjub

  committed
  32c0247

  Copy full SHA for 32c0247

• update documentation

  benjub

  committed
  8de458b

  Copy full SHA for 8de458b

• remove need for deques (unchanged behavior provided -statements are not overridden in the mm database)

  benjub

  committed
  5a23858

  Copy full SHA for 5a23858

• minor

  benjub

  committed
  7c7373b

  Copy full SHA for 7c7373b

Commits on Apr 1, 2022

• minor; remove experimental equal_subst since no gain; add logfile argument

  benjub

  committed
  06808c6

  Copy full SHA for 06808c6

• document code; some streamlining

  benjub

  committed
  187ce76

  Copy full SHA for 187ce76

• typo

  benjub

  committed
  1b01fa2

  Copy full SHA for 1b01fa2

• add comments; update add_f

  benjub

  committed
  9ea0d66

  Copy full SHA for 9ea0d66

• fix comment

  benjub

  committed
  262c5ce

  Copy full SHA for 262c5ce

• fix comment

  benjub

  committed
  836e3a2

  Copy full SHA for 836e3a2

Commits on Apr 2, 2022

• more precise error messages and comments; add entry/exit log messages similar to metamath.c's

  benjub

  committed
  1bf3408

  Copy full SHA for 1bf3408

• remove two uses of 'reversed'; small speedup

  benjub

  committed
  0fd9779

  Copy full SHA for 0fd9779

• check compressed proofs on the fly; ~55% speedup

  benjub

  committed
  ffb533b

  Copy full SHA for ffb533b

• formatting

  benjub

  committed
  a5f0abb

  Copy full SHA for a5f0abb

Commits on Apr 4, 2022

• update code from os.path to pathlib; fix a bug when the database contains an inclusion statement to itself

  benjub

  committed
  73bd241

  Copy full SHA for 73bd241

• variable renaming for clarity

  benjub

  committed
  707a92e

  Copy full SHA for 707a92e

• fix bug when file ends on '$]'

  benjub

  committed
  01817a8

  Copy full SHA for 01817a8

• fix intermediate code mistake (empty list instead of empty set) which apparently had no consequences...

  benjub

  committed
  6c8ca06

  Copy full SHA for 6c8ca06

• fix bug that caused erroneous raised exception message

  benjub

  committed
  e2eab24

  Copy full SHA for e2eab24

• add a comment

  benjub

  committed
  35531a8

  Copy full SHA for 35531a8

• typing

  benjub

  committed
  cd08835

  Copy full SHA for cd08835

• typo

  benjub

  committed
  b5a6686

  Copy full SHA for b5a6686

• variable renaming (stat-->stmt) for consistency; put only vars in dv conditions; the method find_vars belongs to the class FrameStack, not MM

  benjub

  committed
  83769cc

  Copy full SHA for 83769cc

• partially revert previous commit

  benjub

  committed
  ad49aa0

  Copy full SHA for ad49aa0

Commits on Apr 5, 2022

• add typing annotation to pass mypy --strict

  benjub

  committed
  13b401c

  Copy full SHA for 13b401c

• variable renaming to avoid collisions with field names

  benjub

  committed
  4304ada

  Copy full SHA for 4304ada

• convert head comment to module docstring

  benjub

  committed
  96e8564

  Copy full SHA for 96e8564

• some code linting using pylint

  benjub

  committed
  5e01f7f

  Copy full SHA for 5e01f7f

Commits on Apr 6, 2022

• added precisions to head comment

  benjub

  committed
  69c3097

  Copy full SHA for 69c3097

Commits on May 5, 2022

• find_vars: return a set and use set comprehension; 2% faster on set.mm

  benjub

  committed
  96e6df1

  Copy full SHA for 96e6df1

• replace .intersection() with set comprehension tricks; 1% faster on set.mm but ymmv

  benjub

  committed
  0b54499

  Copy full SHA for 0b54499

• remove some confusing comments; variable naming consistency

  benjub

  committed
  84cf129

  Copy full SHA for 84cf129

• variable naming consistency; consistency in the order of the components in the couples (typecode, var)

  benjub

  committed
  277fdd7

  Copy full SHA for 277fdd7

• checking that enough subproofs have been saved

  benjub

  committed
  0999f6a

  Copy full SHA for 0999f6a

• improve consistency: first: typecode, second: variable

  benjub

  committed
  d7d2985

  Copy full SHA for d7d2985

• clarify error message

  benjub

  committed
  72c2b50

  Copy full SHA for 72c2b50

• raise if stack empty at end of proof; clear error messages

  benjub

  committed
  f1ea8f5

  Copy full SHA for f1ea8f5

• review and clarify all raised messages; aggressive autopep8

  benjub

  committed
  a96ed02

  Copy full SHA for a96ed02

• fix bug and better logging

  benjub

  committed
  1e43d5f

  Copy full SHA for 1e43d5f

• improve logging

  benjub

  committed
  4713831

  Copy full SHA for 4713831

• typo

  benjub

  committed
  ba7dd37

  Copy full SHA for ba7dd37