{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":50906927,"defaultBranch":"master","name":"tlaplus","ownerLogin":"tlaplus","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2016-02-02T08:48:27.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/2684289?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1712873071.0","currentOid":""},"activityList":{"items":[{"before":"fa4968f60a0a460da4b7e182330680ce93bd96aa","after":"72c23c95cbf1ae61908628d9dd65b712f1e4e2e0","ref":"refs/heads/master","pushedAt":"2024-05-08T15:11:19.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Algorithm variant has been proven in \"Refinement Proofs in Rust Using Ghost Locks\"\n\nAddresses Github issue #916\r\nhttps://github.com/tlaplus/tlaplus/issues/916\r\n\r\n[Documentation][TLC]","shortMessageHtmlLink":"Algorithm variant has been proven in \"Refinement Proofs in Rust Using…"}},{"before":"03c7bf4f35ccf1217ac2c53e5bf60d1220c8b0d8","after":"fa4968f60a0a460da4b7e182330680ce93bd96aa","ref":"refs/heads/master","pushedAt":"2024-04-27T22:40:18.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Use Java 11 but not specific version in CI\n\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Use Java 11 but not specific version in CI"}},{"before":"e44242262b02d6c28127171fc8be0ca3249267fd","after":"99e6322cd152c44dec03677c51f45728a4041539","ref":"refs/heads/cal-gh835-bufferedrandomaccessfile","pushedAt":"2024-04-24T22:01:33.000Z","pushType":"push","commitsCount":4,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Add a focused, well-documented test for setLength pointer interaction\n\nSigned-off-by: Calvin Loncaric ","shortMessageHtmlLink":"Add a focused, well-documented test for setLength pointer interaction"}},{"before":"197b11a7b0ac17afcdd01f36b680be848d55e8de","after":"e44242262b02d6c28127171fc8be0ca3249267fd","ref":"refs/heads/cal-gh835-bufferedrandomaccessfile","pushedAt":"2024-04-23T21:36:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Simplify `TruncateOrExtendFile`\n\nSigned-off-by: Calvin Loncaric ","shortMessageHtmlLink":"Simplify TruncateOrExtendFile"}},{"before":"297c4c8350a2c6cf76830f20e89b0618cd8bcfb7","after":"197b11a7b0ac17afcdd01f36b680be848d55e8de","ref":"refs/heads/cal-gh835-bufferedrandomaccessfile","pushedAt":"2024-04-23T21:01:43.000Z","pushType":"push","commitsCount":6,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Note a potential optimization opportunity\n\nSigned-off-by: Calvin Loncaric ","shortMessageHtmlLink":"Note a potential optimization opportunity"}},{"before":"4b513adab1fc94f4cdfffbcff4e39f1fe3e8932b","after":"03c7bf4f35ccf1217ac2c53e5bf60d1220c8b0d8","ref":"refs/heads/master","pushedAt":"2024-04-20T13:10:30.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Fix CI in response to breaking changes in tlaplus/examples repo\n\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Fix CI in response to breaking changes in tlaplus/examples repo"}},{"before":"6fb13e9d0e5d35ac7ad6d5beab8ae94e3dcdde96","after":"4b513adab1fc94f4cdfffbcff4e39f1fe3e8932b","ref":"refs/heads/master","pushedAt":"2024-04-18T00:25:49.000Z","pushType":"pr_merge","commitsCount":5,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Use nio file API in pcal.trans\n\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Use nio file API in pcal.trans"}},{"before":"0cbbd06847de6f2d47b631f55806ce20baa7541b","after":null,"ref":"refs/heads/mku-DebuggerINotInModelFunctor","pushedAt":"2024-04-11T22:04:31.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"}},{"before":"f135b2c6db08b31be45e3ab217213d9a03d75414","after":"6fb13e9d0e5d35ac7ad6d5beab8ae94e3dcdde96","ref":"refs/heads/master","pushedAt":"2024-04-11T21:12:52.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"'constrained' states not added to e.g. dot output if TLC runs under TLA+\ndebugger.\n\nRelated to git commit c2713def38aa1d3255a6c2fe2aa037253e00e361\n\nHave DebugTool implement INotInModelFunctor.\n\n[Bug][TLC]\n\nSigned-off-by: Markus Alexander Kuppe ","shortMessageHtmlLink":"'constrained' states not added to e.g. dot output if TLC runs under TLA+"}},{"before":"8fa1f19c4d4a1da46d4212208cd9249e96f14fb5","after":"f135b2c6db08b31be45e3ab217213d9a03d75414","ref":"refs/heads/master","pushedAt":"2024-04-11T20:57:18.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Fix unit test error reporting and support `-Dthreads=N` parameter (#903)\n\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Fix unit test error reporting and support -Dthreads=N parameter (#903)"}},{"before":null,"after":"0cbbd06847de6f2d47b631f55806ce20baa7541b","ref":"refs/heads/mku-DebuggerINotInModelFunctor","pushedAt":"2024-04-11T18:56:55.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"'constrained' states not added to e.g. dot output if TLC runs under TLA+\ndebugger.\n\nRelated to git commit c2713def38aa1d3255a6c2fe2aa037253e00e361\n\nHave DebugTool implement INotInModelFunctor.\n\n[Bug][TLC]\n\nSigned-off-by: Markus Alexander Kuppe ","shortMessageHtmlLink":"'constrained' states not added to e.g. dot output if TLC runs under TLA+"}},{"before":"cd7cf923a2afbf0ee5fdc2a6ca36f5b80438f318","after":"297c4c8350a2c6cf76830f20e89b0618cd8bcfb7","ref":"refs/heads/cal-gh835-bufferedrandomaccessfile","pushedAt":"2024-04-10T21:54:33.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Rework `BufferedRandomAccessFile`\n\nThis commit makes major alterations to `BufferedRandomAccessFile` to\nbring it in line with the general `RandomAccessFile` contract:\n\n - Invariant V1 has been strengthened to include a contract for the\n `length` field.\n\n - Invariants V2-V5 have been altered to account for cases where\n `curr > length`, which the `RandomAccessFile` contract allows.\n\n - Additionally, invariant V5 has been adjusted to clarify that\n `dirty=true` does not imply that there are unflushed bytes. The\n implication is only one-way: if there are unflushed bytes, then\n `dirty=true`.\n\n - The `hi` and `maxHi` fields have been removed. These largely\n duplicate information that can be quickly recomputed, meaning they\n add additional complexity to the class invariants. Without those\n fields, invariant V6 can be removed.\n\n - The `close()` method now closes the underlying file descriptor even\n if `flush()` throws an exception.\n\nDue to the complexity of this change, I have added a TLA+ specification\nfor `BufferedRandomAccessFile` to enable model checking of its design.\n\nTo ensure that the code is correct, this commit also adds a substantial\namount of test infrastructure:\n\n - Several new regression tests have been added. These are a little\n cryptic because they were randomly generated, but they do reflect\n true behaviors of the `RandomAccessFile` contract.\n\n - A fuzz test has been added. This test ensures that many sequences\n of random operations behave correctly. It also minimizes failures\n so they can be easily converted to regression tests.\n\nThis commit also makes some whitespace and formatting adjustments.\n\nFixes #835. I have verified that the tests now pass under Java 21.\n\nSigned-off-by: Calvin Loncaric ","shortMessageHtmlLink":"Rework BufferedRandomAccessFile"}},{"before":null,"after":"cd7cf923a2afbf0ee5fdc2a6ca36f5b80438f318","ref":"refs/heads/cal-gh835-bufferedrandomaccessfile","pushedAt":"2024-04-10T21:51:41.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Rework `BufferedRandomAccessFile`\n\nThis commit makes major alterations to `BufferedRandomAccessFile` to\nbring it in line with the general `RandomAccessFile` contract:\n\n - Invariant V1 has been strengthened to include a contract for the\n `length` field.\n\n - Invariants V2-V5 have been altered to account for cases where\n `curr > length`, which the `RandomAccessFile` contract allows.\n\n - Additionally, invariant V5 has been adjusted to clarify that\n `dirty=true` does not imply that there are unflushed bytes. The\n implication is only one-way: if there are unflushed bytes, then\n `dirty=true`.\n\n - The `hi` and `maxHi` fields have been removed. These largely\n duplicate information that can be quickly recomputed, meaning they\n add additional complexity to the class invariants. Without those\n fields, invariant V6 can be removed.\n\n - The `close()` method now closes the underlying file descriptor even\n if `flush()` throws an exception.\n\nDue to the complexity of this change, I have added a TLA+ specification\nfor `BufferedRandomAccessFile` to enable model checking of its design.\n\nTo ensure that the code is correct, this commit also adds a substantial\namount of test infrastructure:\n\n - Several new regression tests have been added. These are a little\n cryptic because they were randomly generated, but they do reflect\n true behaviors of the `RandomAccessFile` contract.\n\n - A fuzz test has been added. This test ensures that many sequences\n of random operations behave correctly. It also minimizes failures\n so they can be easily converted to regression tests.\n\nThis commit also makes some whitespace and formatting adjustments.\n\nFixes #835. I have verified that the tests now pass under Java 21.","shortMessageHtmlLink":"Rework BufferedRandomAccessFile"}},{"before":"b9b30bbfef62f6d218f83df839efe440dc842e3f","after":"8fa1f19c4d4a1da46d4212208cd9249e96f14fb5","ref":"refs/heads/master","pushedAt":"2024-04-10T17:19:19.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Add unicode support to SANY (#896)\n\nSome of the files in this changeset are autogenerated from `tla+.jj`:\r\n - `TLAplusParser.java`\r\n - `TLAplusParserConstants.java`\r\n - `TLAplusParserTokenManager.java`\r\n\r\nMostly these changes just involved adding unicode lexeme options to the\r\ndefinitions in `tla+.jj`, and adding unicode operator synonyms to\r\n`ConfigConstants.java`. The only parsing logic changes were in\r\n`BracketStack.java`, where I just changed it from storing the token end\r\ncolumn to the token start column. My main fear was that JavaCC would\r\nuse byte offsets instead of codepoint offsets to calculate columns, but\r\nhappily they use codepoints! So everything really was almost too easy.\r\n\r\nThere were also some simple changes to the level-checking AST\r\ngeneration code in `semantic/Generator.java`. It branched based on the\r\nASCII value of some constructs; I switched it to use the parser node\r\nkind. These errors were caught by the tlaplus/examples integration\r\ntests described below.\r\n\r\nFor testing, I added a whole bunch of unicode cases to the syntax\r\ncorpus parsing test. I also added a job to the PR CI so it runs the\r\ntlaplus/examples integration tests after converting all the specs to\r\nunicode with TLAUC. This runs in parallel to the other jobs so does not\r\nincrease CI run time.\r\n\r\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Add unicode support to SANY (#896)"}},{"before":"ccac18b796b19fce07b04c04516ba0d3e63260b3","after":null,"ref":"refs/heads/fix-testWriteIndex","pushedAt":"2024-04-10T00:38:58.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"}},{"before":"d1504b6dc0ed35e3d4d343a3d380d0f4fe4980e9","after":"b9b30bbfef62f6d218f83df839efe440dc842e3f","ref":"refs/heads/master","pushedAt":"2024-04-10T00:38:55.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Fix `OffHeapDiskFPSetTest.testWriteIndex()` on Java 21\n\nIn Java 21 the various `RandomAccessFile` read methods like\n`readLong()` are now implemented using bulk array reads, not\nsingle-byte reads. Therefore, `DummyRandomAccessFile` needs to\nimplement those methods if it is to function as intended.\n\nSigned-off-by: Calvin Loncaric ","shortMessageHtmlLink":"Fix OffHeapDiskFPSetTest.testWriteIndex() on Java 21"}},{"before":"53ba1f7d88fb2d315979cdf916d0635c8033f721","after":"ccac18b796b19fce07b04c04516ba0d3e63260b3","ref":"refs/heads/fix-testWriteIndex","pushedAt":"2024-04-09T23:56:27.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Fix `OffHeapDiskFPSetTest.testWriteIndex()` on Java 21\n\nIn Java 21 the various `RandomAccessFile` read methods like\n`readLong()` are now implemented using bulk array reads, not\nsingle-byte reads. Therefore, `DummyRandomAccessFile` needs to\nimplement those methods if it is to function as intended.\n\nSigned-off-by: Calvin Loncaric ","shortMessageHtmlLink":"Fix OffHeapDiskFPSetTest.testWriteIndex() on Java 21"}},{"before":null,"after":"53ba1f7d88fb2d315979cdf916d0635c8033f721","ref":"refs/heads/fix-testWriteIndex","pushedAt":"2024-04-09T23:50:23.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Fix `OffHeapDiskFPSetTest.testWriteIndex()` on Java 21\n\nIn Java 21 the various `RandomAccessFile` read methods like\n`readLong()` are now implemented using bulk array reads, not\nsingle-byte reads. Therefore, `DummyRandomAccessFile` needs to\nimplement those methods if it is to function as intended.\n\nSigned-off-by: Calvin Loncaric ","shortMessageHtmlLink":"Fix OffHeapDiskFPSetTest.testWriteIndex() on Java 21"}},{"before":null,"after":"d035b25db314f94ac2544c0b49efef7a5e712748","ref":"refs/heads/cal/maven-build-system","pushedAt":"2024-04-08T19:48:08.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Add prototype pom.xml","shortMessageHtmlLink":"Add prototype pom.xml"}},{"before":"0f27f0bdb4864ec92654abf49362e565e332b71e","after":"d1504b6dc0ed35e3d4d343a3d380d0f4fe4980e9","ref":"refs/heads/master","pushedAt":"2024-04-08T00:43:22.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Skip EWD998ChanTrace model that does not run because it doesn't find its .ndjson input when it's run outside of tlaplus/Examples.\n\nRelated to Github issue #134 (tlaplus/Examples)\nhttps://github.com/tlaplus/Examples/issues/134\n\n[Build]\n\nSigned-off-by: Markus Alexander Kuppe ","shortMessageHtmlLink":"Skip EWD998ChanTrace model that does not run because it doesn't find …"}},{"before":"704bd4d190553bc65d307cac862a5c41395c8ff8","after":"0f27f0bdb4864ec92654abf49362e565e332b71e","ref":"refs/heads/master","pushedAt":"2024-04-05T00:21:00.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Use JavaCC to generate TLA+ parser files during build (#876)\n\n[Build]\r\n\r\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Use JavaCC to generate TLA+ parser files during build (#876)"}},{"before":"698cb8abea2dd3070a4c518095fa22fbeeda4e04","after":"704bd4d190553bc65d307cac862a5c41395c8ff8","ref":"refs/heads/master","pushedAt":"2024-04-04T22:25:10.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Calvin-L","name":"Calvin Loncaric","path":"/Calvin-L","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/1393639?s=80&v=4"},"commit":{"message":"Parallelize unit tests (#902)\n\nThis was actually easier than expected (edit: it was not easier than\r\nexpected). Somehow I missed that the JUnit task has a `threads`\r\nparameter. I guess this is a newer addition which is why not a lot of\r\ndocumentation mentions it. Now the unit test target will run with\r\nnumber of threads equal to available cores on the machine. Decent\r\nimprovement, unit tests finish in less than 10 minutes now which puts\r\nthem below the time of the tlaplus/examples integration tests! There\r\nwere a few small changes I had to make to some tests to ensure they\r\ndon't interfere with each other with operations on the `states`\r\nmetadir.\r\n\r\nI also added a useful python script to run during the CI after the\r\ntests; it:\r\n\r\n - Prints the total number of tests and total number of failed tests\r\n - Prints out any tests that were run multiple times by mistake\r\n - Prints out the top-20 longest-running tests and their runtimes\r\n - If any tests failed, fetches all the error info from the xml file in\r\n the surefire runner directory and prints it to console\r\n\r\nI made the following changes to the ant build:\r\n\r\n - Added a separate sequential unit test target that runs before the\r\n parallelized unit test target, for tests which cannot be\r\n parallelized for whatever reason (exclusively bind to a system\r\n network port or something).\r\n - Ensure all unit tests run even if some fail by not passing in the\r\n `-Dtest.halt=true` parameter; previously the tests would stop at the\r\n first failure, which IMO is not as useful for debugging. This\r\n necessitated adding a conditional `fail` target under the test\r\n targets, which activates when `failureproperty` is set in the\r\n `junit` target. This ensures the CI still fails with nonzero exit\r\n code upon any failures.\r\n - Moved the longest-running tests first so their execution is covered\r\n by the concurrent execution of other tests and doesn't\r\n singlehandedly cause the unit tests to run for an additional minute\r\n or whatever.\r\n\r\nI ran this workflow locally on my 8-thread workstation over 10 times so\r\nI have fairly high confidence there aren't any other concurrency\r\nfailures lurking.\r\n\r\nCloses #901\r\n\r\n[Build]\r\n\r\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Parallelize unit tests (#902)"}},{"before":"23f765078cd098a2bc2bc3d19889ba0c64583ca4","after":"698cb8abea2dd3070a4c518095fa22fbeeda4e04","ref":"refs/heads/master","pushedAt":"2024-04-01T18:13:03.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Parallelize PR CI workflow (#900)\n\nParallelize PR CI workflow\r\n\r\n[Build]\r\n\r\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Parallelize PR CI workflow (#900)"}},{"before":"84f0705fc886c008e9ac6e20074e45343f20c461","after":null,"ref":"refs/heads/mku-progress","pushedAt":"2024-03-26T04:20:52.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"}},{"before":"677e994484544618a145f6b2f11cf62f10622b39","after":"23f765078cd098a2bc2bc3d19889ba0c64583ca4","ref":"refs/heads/master","pushedAt":"2024-03-26T04:20:49.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Add TLC hook to periodically evaluate a constant-level expression.\n\nThis hook can be set up using the (provisional) `_PERIODIC` keyword\nwithin the configuration file.\n\n[Feature][TLC]\n\nSigned-off-by: Markus Alexander Kuppe ","shortMessageHtmlLink":"Add TLC hook to periodically evaluate a constant-level expression."}},{"before":"aebc933327790d8372aa6108686e76b8d17452ca","after":"84f0705fc886c008e9ac6e20074e45343f20c461","ref":"refs/heads/mku-progress","pushedAt":"2024-03-26T03:45:35.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Add TLC hook to periodically evaluate a constant-level expression.\n\nThis hook can be set up using the (provisional) `_PERIODIC` keyword\nwithin the configuration file.\n\n[Feature][TLC]\n\nSigned-off-by: Markus Alexander Kuppe ","shortMessageHtmlLink":"Add TLC hook to periodically evaluate a constant-level expression."}},{"before":"e8241f7774e3238b7f147dd1a6c395eb7085f634","after":"aebc933327790d8372aa6108686e76b8d17452ca","ref":"refs/heads/mku-progress","pushedAt":"2024-03-26T03:40:33.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Add TLC hook to periodically evaluate a constant-level expression.\n\nThis hook can be set up using the (provisional) `_PERIODIC` keyword\nwithin the configuration file.\n\n[Feature][TLC]\n\nSigned-off-by: Markus Alexander Kuppe ","shortMessageHtmlLink":"Add TLC hook to periodically evaluate a constant-level expression."}},{"before":null,"after":"e8241f7774e3238b7f147dd1a6c395eb7085f634","ref":"refs/heads/mku-progress","pushedAt":"2024-03-26T01:54:33.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Add TLC hook to periodically evaluates a constant-level expression.\n\nThis hook can be set up using the (provisional) `_PERIODIC` keyword\nwithin the configuration file.\n\n[Feature][TLC]\n\nSigned-off-by: Markus Alexander Kuppe ","shortMessageHtmlLink":"Add TLC hook to periodically evaluates a constant-level expression."}},{"before":"95d01059883140eb76d09fd056ad99d468adf750","after":"677e994484544618a145f6b2f11cf62f10622b39","ref":"refs/heads/master","pushedAt":"2024-03-24T16:05:19.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Statically initialize operators table (#895)\n\nStatically initialize operators table, to enable implementing Unicode support for SANY.\r\n\r\nRemoves ability to specify operator parse precedence from config.src file, which is believed to be an unsed SANY feature.\r\n\r\nRelated: https://github.com/tlaplus/tlaplus/pull/896\r\n\r\n[Refactor][SANY][Changelog]\r\n\r\nSigned-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com>","shortMessageHtmlLink":"Statically initialize operators table (#895)"}},{"before":"3c119e1504e146f8dbe8637cf4d548e5f5e4630a","after":"95d01059883140eb76d09fd056ad99d468adf750","ref":"refs/heads/master","pushedAt":"2024-03-23T06:14:03.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"lemmy","name":"Markus Alexander Kuppe","path":"/lemmy","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/88777?s=80&v=4"},"commit":{"message":"Expose `Json!ndJsonSerialize` also under `IOUtils!Serialize` to support\nappending lines to an existing ndjson file.\n\n```tla\nSerialize(<<\"bar\">>, \"test.ndjson\", [format |-> \"NDJSON\", charset |->\n\"UTF-8\", openOptions |-> <<\"WRITE\", \"CREATE\", \"APPEND\">>])\n```\n\nBased on:\nhttps://github.com/tlaplus/tlaplus/commit/f4803418873d02f14ce3fa5f2849839a454a1aa9\nhttps://github.com/tlaplus/tlaplus/commit/224936696851dd4ec8ea2e49e81fee32140afc52\n\n[Feature][TLC]\n\nSigned-off-by: Markus Alexander Kuppe ","shortMessageHtmlLink":"Expose Json!ndJsonSerialize also under IOUtils!Serialize to support"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAERMRcLwA","startCursor":null,"endCursor":null}},"title":"Activity · tlaplus/tlaplus"}