Code

doc: various docs and docs page#17

Code

Merged

ramonfmir merged 52 commits intomainverified-optimization/CvxLean:mainfrom docs-and-clean-upverified-optimization/CvxLean:docs-and-clean-upCopy head branch name to clipboardFeb 6, 2024

Commits

Commits on Jan 31, 2024

• style: same style for all case studies

  ramonfmir

  committed
  d77b8ba

  Copy full SHA for d77b8ba

• chore: move result about Fin

  ramonfmir

  committed
  7197860

  Copy full SHA for 7197860

• feat: custom errors and debugging

  ramonfmir

  committed
  c67bda4

  Copy full SHA for c67bda4

• doc: Coeffs.lean

  ramonfmir

  committed
  539a21c

  Copy full SHA for 539a21c

• fix: use "positive" and "nonneg" correctly

  ramonfmir

  committed
  e128b0e

  Copy full SHA for e128b0e

Commits on Feb 1, 2024

• doc: Command/Solve/Float

  ramonfmir

  committed
  90572b1

  Copy full SHA for 90572b1

• doc: Command/Solve/Mosek

  ramonfmir

  committed
  3d9d826

  Copy full SHA for 3d9d826

• doc: Command/Solve

  ramonfmir

  committed
  caa5bb4

  Copy full SHA for caa5bb4

• doc: Command/Solve.lean

  ramonfmir

  committed
  662ad7a

  Copy full SHA for 662ad7a

• feat: @[strong_equiv], @[equiv], @[red], and @[rel]

  ramonfmir

  committed
  7b4ee65

  Copy full SHA for 7b4ee65

• feat: use equiv theorems to reduce computable backward map

  ramonfmir

  committed
  91d95de

  Copy full SHA for 91d95de

• feat: more custom error commands

  ramonfmir

  committed
  d1d15ce

  Copy full SHA for d1d15ce

Commits on Feb 2, 2024

• doc: everything in Command

  ramonfmir

  committed
  3b4e9d2

  Copy full SHA for 3b4e9d2

Commits on Feb 3, 2024

• chore: bump to v4.6.0-rc1 and update mathlib

  ramonfmir

  committed
  a7b4d33

  Copy full SHA for a7b4d33

• wip: fixing proofs, no Abs

  ramonfmir

  committed
  db410b2

  Copy full SHA for db410b2

• fix: all proofs fixed

  ramonfmir

  committed
  50dc619

  Copy full SHA for 50dc619

• fix: log_le_log_iff

  ramonfmir

  committed
  3a66d96

  Copy full SHA for 3a66d96

Commits on Feb 4, 2024

• fix: confusion between real and vector norms

  ramonfmir

  committed
  ec9ebed

  Copy full SHA for ec9ebed

• fix: reduction backward maps

  ramonfmir

  committed
  15672a1

  Copy full SHA for 15672a1

• feat: computable matrix inverse

  ramonfmir

  committed
  7191b0c

  Copy full SHA for 7191b0c

• feat: recovering all original solutions in case studies

  ramonfmir

  committed
  ae3c24a

  Copy full SHA for ae3c24a

• fix: tests passing

  ramonfmir

  committed
  6d9a372

  Copy full SHA for 6d9a372

• feat: do not norm_num too much

  ramonfmir

  committed
  a413785

  Copy full SHA for a413785

• feat: more custom errors

  ramonfmir

  committed
  1f24e96

  Copy full SHA for 1f24e96

• feat: better error messages in rw_obj, rw_constr, and pre_dcp

  ramonfmir

  committed
  ec17efe

  Copy full SHA for ec17efe

• fix: one unit test needed more heartbeats

  ramonfmir

  committed
  6340942

  Copy full SHA for 6340942

• doc: case studies

  ramonfmir

  committed
  bc874f5

  Copy full SHA for bc874f5

• doc: Meta/Util and some refactor

  ramonfmir

  committed
  459b995

  Copy full SHA for 459b995

• doc: Meta

  ramonfmir

  committed
  2eed96a

  Copy full SHA for 2eed96a

• doc: some Lib

  ramonfmir

  committed
  242fa18

  Copy full SHA for 242fa18

• doc: Lib

  ramonfmir

  committed
  43b7bb5

  Copy full SHA for 43b7bb5

• doc: Syntax

  ramonfmir

  committed
  fec4e50

  Copy full SHA for fec4e50

• fix: p and q in EquivalenceExpr are now lhs and rhs

  ramonfmir

  committed
  939dac5

  Copy full SHA for 939dac5

• chore: remove SciLean test

  ramonfmir

  committed
  dffe7a7

  Copy full SHA for dffe7a7

• chore: remove CvxLean.code-workspace

  ramonfmir

  committed
  ff99606

  Copy full SHA for ff99606

• chore: ignore *.code-workspace

  ramonfmir

  committed
  1dc1be1

  Copy full SHA for 1dc1be1

• wip: more hearbeats needed in pre_dcp, issue with new norm_num_clean_up?

  ramonfmir

  committed
  e4a674c

  Copy full SHA for e4a674c

• feat: norm_num while converting

  ramonfmir

  committed
  4df5a9b

  Copy full SHA for 4df5a9b

• wip: generate docs

  ramonfmir

  committed
  3919d13

  Copy full SHA for 3919d13

• fix: labels in constraint in doc

  ramonfmir

  committed
  bdedb7c

  Copy full SHA for bdedb7c

• style: no auto-implicit

  ramonfmir

  committed
  8b1548b

  Copy full SHA for 8b1548b

• wip: no pp options, for now

  ramonfmir

  committed
  abbf7e5

  Copy full SHA for abbf7e5

Commits on Feb 6, 2024

• wip: generate docs in CI

  ramonfmir

  committed
  88a3783

  Copy full SHA for 88a3783

• chore: update toolchain in CI

  ramonfmir

  committed
  00c5703

  Copy full SHA for 00c5703

• fix: path in docs CI

  ramonfmir

  committed
  8850197

  Copy full SHA for 8850197

• fix: implicit argument order in real-to-float conversion

  ramonfmir

  committed
  81abd80

  Copy full SHA for 81abd80

• fix: no auto-implicit in tests

  ramonfmir

  committed
  9549aac

  Copy full SHA for 9549aac

• wip: do not show label

  ramonfmir

  committed
  29bd7ed

  Copy full SHA for 29bd7ed

• fix: order of arguments in vecMul and mulVec

  ramonfmir

  committed
  e0a2a79

  Copy full SHA for e0a2a79

• fix: copy-paste issues in docs CI

  ramonfmir

  committed
  95dab21

  Copy full SHA for 95dab21

• fix: explicit checkout path in docs action

  ramonfmir

  committed
  4515c5a

  Copy full SHA for 4515c5a

• fix: working directory in build

  ramonfmir

  committed
  5b96d36

  Copy full SHA for 5b96d36