In tsx with generic, delete or new method makes "Unexpected token Some(JSXTagStart)" Error

Describe the bug
I have written code that uses generics, but swc seems to recognize it as a jsx tag.
Input code
class A {
  delete<T>() {}
}

or
class A {
  new<T>() {}
}

Config
{
  "jsc": {
    "parser": {
      "syntax": "typescript",
      "tsx": true,
      "decorators": true
    }
  }
}

Expected behavior
expected successful compilation like babel or ts-loader
babel example
But it makes that error:
error: Unexpected token Some(JSXTagStart)
 --> index.ts:2:9
  |
2 |   delete<T>() {}
  |         ^

[Error: failed to process js file

Caused by:
    failed to parse module]

Version
The version of @swc/core: 1.2.19
Additional context

Yep, really strange behavior - even in .ts files.

this problem seems to have been fixed.
ps: I failed to reproduce #2099 ,that may be another problem

Closing as fixed by https://github.com/swc-project/swc/pull/2076


Correct subscription flow

I'm trying to setup a subscription for my app. I've been following this example https://github.com/charliecruzan-stripe/react-native-video-series/ with the PaymentSheetSubscription.tsx file.
What's happening now is that the subscription is started as soon as the page is open, since await stripe.subscriptions.create() is called.
What I want is to:

Collect payment info
Start the subscription starting with the free trial

What should be the correct flow to follow? It isn't clear at all from any documentation

I think you might be looking for setup intents- https://stripe.com/docs/payments/setup-intents


improve readme

sry, forgot to push – fixes previous typo and adds gitignore

Oops. make does not work any more ...
$ make
cc   fix-perspective.o intersect-lines-2d.o fix-perspective.cpp  -lopencv_stitching -lopencv_alphamat -lopencv_aruco -lopencv_bgsegm -lopencv_bioinspired -lopencv_ccalib -lopencv_dnn_objdetect -lopencv_dnn_superres -lopencv_dpm -lopencv_face -lopencv_freetype -lopencv_fuzzy -lopencv_hdf -lopencv_hfs -lopencv_img_hash -lopencv_intensity_transform -lopencv_line_descriptor -lopencv_mcc -lopencv_quality -lopencv_rapid -lopencv_reg -lopencv_rgbd -lopencv_saliency -lopencv_shape -lopencv_stereo -lopencv_structured_light -lopencv_phase_unwrapping -lopencv_superres -lopencv_optflow -lopencv_surface_matching -lopencv_tracking -lopencv_highgui -lopencv_datasets -lopencv_text -lopencv_plot -lopencv_ml -lopencv_videostab -lopencv_videoio -lopencv_viz -lopencv_ximgproc -lopencv_video -lopencv_dnn -lopencv_xobjdetect -lopencv_objdetect -lopencv_calib3d -lopencv_imgcodecs -lopencv_features2d -lopencv_flann -lopencv_xphoto -lopencv_photo -lopencv_imgproc -lopencv_core -o fix-perspective
fix-perspective.cpp:6:10: fatal error: opencv2/core/mat.hpp: Datei oder Verzeichnis nicht gefunden
    6 | #include <opencv2/core/mat.hpp>
      |          ^~~~~~~~~~~~~~~~~~~~~~
compilation terminated.
make: *** [<eingebaut>: fix-perspective] Fehler 1

Oops. make does not work any more ...

It should look like this:
$ make
g++ -I/usr/local/include/opencv4 -I/usr/include/eigen3 -g -Wall -Wextra -MMD   -c -o intersect-lines-2d.o intersect-lines-2d.cpp
g++ -I/usr/local/include/opencv4 -I/usr/include/eigen3 -g -Wall -Wextra -MMD    fix-perspective.cpp intersect-lines-2d.o  -L/usr/local/lib -lopencv_dnn -lopencv_gapi -lopencv_highgui -lopencv_ml -lopencv_objdetect -lopencv_photo -lopencv_stitching -lopencv_video -lopencv_calib3d -lopencv_features2d -lopencv_flann -lopencv_videoio -lopencv_imgcodecs -lopencv_imgproc -lopencv_core -o fix-perspective

(This is with GNU make 4.1.)
Since it calls cc instead of c++ or g++, I assume there is either a problem with the internal ruleset of make (older version?), or the C++ compiler is not installed properly.
What does make -p |& grep -B6 LINK.cpp say?

after make clean it works.


tar to stdout prints "removing leading / from member names"

Using tar as tar cf - /bin/sh or similar, I could not get the archive recognised, doing a hexdump I realised it was outputing the warning to stdout before the archive, which is not very helpful:
00000000  72 65 6d 6f 76 69 6e 67  20 6c 65 61 64 69 6e 67  |removing leading|
00000010  20 27 2f 27 20 66 72 6f  6d 20 6d 65 6d 62 65 72  | '/' from member|
00000020  20 6e 61 6d 65 73 0a 62  69 6e 2f 73 68 00 00 00  | names.bin/sh...|
00000030  00 00 00 00 00 00 00 00  00 00 00 00 00 00 00 00  |................|

On 11/19/2016 10:06 AM, Justin Cormack wrote:

Using |tar| as |tar cf - /bin/sh| or similar, I could not get the
archive recognised, doing a hexdump I realised it was outputing the
warning to stdout before the archive, which is not very helpful:

I note that "toys/pending" is toybox what "drivers/staging" is to the
linux kernel. It has a README to that effect, and current releases
produce a red warning when you build code out of it.
I would love to get tar out of pending (see
http://landley.net/toybox/cleanup.html for the kind of work that
generally involves), but toybox has never been my day job. I've gotten
to work on it half-time in work contexts a couple times, but the past
few months have been insane with non-toybox work commitments. (I was in
Japan for 2 weeks, flew back in time to vote, got on a plane to
minneapolis 2 days later, got back from that monday, and am currently
scheduled to fly to california on tuesday, and from there probably to
san diego. I might get back to Austin around December 10th, just in time
for a road trip.)
tl;dr I can fix this specific bug (done), but until I find time to clean
up tar and move it out of pending I wouldn't rely on it too heavily.
Rob
(The annoying part is if I do an hour's worth of work without getting to
a good checkin point, and I don't get back to it for a couple days, it
can take an hour of reading and fiddling with the code to refamiliarize
myself with enough context/details to figure out where I left off and
why. I need large contiguous chunks of time/energy to do some kinds of
work, those have all been spoken for recently.)

Sorry, I didn't notice it was in pending, I built tar using the nice standalone build mode rather than through the config. Thanks for fixing it, appreciate your time.


Mbox multichannel support

Repairs reading of correct data channel.
- MU_ReceiveMsgNonBlocking(config->base, 0);
+MU_ReceiveMsgNonBlocking(config->base, i_channel);

Repairs calling callback function only when proper flag is set.
Move call into if condition:
if (data->cb[i_channel]) {
    data->cb[i_channel](dev, i_channel, data->user_data[i_channel],
				  &nxp_mu_device_table[dev_id].msg);
}

Adds sample samples/drivers/mbox_data/ as reference to transfer data via mbox.
Adds test tests/drivers/mbox/mbox_data/ to verify mbox data transfer functionality.
---- Opened the serial port /dev/ttyACM0 ----
*** Booting Zephyr OS build zephyr-v3.5.0-4054-gb992fb07f760 ***
Running TESTSUITE mbox_data_tests
=======================�========================================
START - test_ping_pong_1
 PASS - test_ping_pong_1 in 0.001 seconds
===================================================================
START - test_ping_pong_2
 PASS - test_ping_pong_2 in 0.001 seconds
===================================================================
START - test_ping_pong_3
 PASS - test_ping_pong_3 in 0.001 seconds
===================================================================
START - test_ping_pong_4
 PASS - test_ping_pong_4 in 0.001 seconds
===================================================================
TESTSUITE mbox_data_tests succeeded

------ TESTSUITE SUMMARY START ------

SUITE PASS - 100.00% [mbox_data_tests]: pass = 4, fail = 0, skip = 0, total = 4 duration = 0.004 seconds
 - PASS - [mbox_data_tests.test_ping_pong_1] duration = 0.001 seconds
 - PASS - [mbox_data_tests.test_ping_pong_2] duration = 0.001 seconds
 - PASS - [mbox_data_tests.test_ping_pong_3] duration = 0.001 seconds
 - PASS - [mbox_data_tests.test_ping_pong_4] duration = 0.001 seconds

------ TESTSUITE SUMMARY END ------

===================================================================
PROJECT EXECUTION SUCCESSFUL

@kartben Hi, I incorporated yours comments. If you checked them and are OK from your side, could you provide second approve? Thanks


Supervised UMAP using already projected points as regression

Hey Leland,
Thanks for this great library, and for being so responsive with issues.
Question: Is it possible to train a (semi-)supervised UMAP model where some of the projections are already known/provided, as a regression task? This is contrast to using labels for supervision, which are categorical.
To provide an example, imagine I had a set of 100 embeddings. 50 of those embeddings have 2d coordinates associated with them; the other 50 do not. I want to be able to train a UMAP model on the 50 embeddings with 2d coordinates, and then run inference on the other 50 (or do a semi-supervised training and run on all of them at the same time).
If this isn't feasible with UMAP, do you know of any other algos/models that might be a good fit for what I'm suggesting (besides deep learning of course)?
Thanks! Amol

There are two ways you can view this. The 2d coordinates could be viewed merely as target values, like labels but numeric instead of categorical. This can actually be handled just fine by setting target_metric="euclidean" and passing the coordinates in as a y value to fit. I don't think this is what you mean however.
Instead it sounds more like you want to fix some of the points to given locations in the embedding and then fit the rest of the points around that. This is actually being worked on right now. See #606 and #620 for discussion and work on that. There are some catches in exactly how to do this so I think your input into this would be most welcome.

Thanks for the response, and sorry for my delayed post.
You're right that fixing points is closer to what I need. But I can play around with the first suggestion, using a euclidean target_metric. Does that support semi-supervised cases? In the documentation (https://umap-learn.readthedocs.io/en/latest/supervised.html) you describe using -1 as a 'masked' value. Makes sense for categorical data, but how does that work for numerical data?

The semi-supervised case is going to be an issue for other target_metrics since they won't specially handle "masked" values. In principle you can write your own custom metric that has special handling for masked values. I suspect in the long run this is going to really be doing what you want however.

If checks pass on #620 is that sufficient to merge into the library? Or do you feel there is more to be done there? I had a look over the code in that PR, though admittedly a lot of the math flew over my head.

There are some slightly more philosophical and API issues that need to get worked out before it gets merged, but you can certainly just check out the branch from the PR and use it -- it works; it just requires a little care from the user or unexpected results may occur.

To expand on @lmcinnes API/philosopy comment:  I started using #620, but now am favoring a more flexible API style, inspired by the PyMDE constraints objects.
Passing UMAP constraint objects also can avoid some jit-related code duplication in #620. So one cleaner API might just add an optional constraint parameter, where constraint objects have a few standard project_foo functions.  Constraint (The constraint parameter might end up being a dict, indicating how/when the project_foo functions of several constraints get called: do they operate on gradients, or individual embedding mods, or post-epoch point-cloud, ...?)  Like PyMDE, we'd supply a couple of handy constraints to get folks up and running.
In a first example, I've used a pin_mask (uggh, will change!) to anchor "my selected anchors" at left/right best/worst x limits, leaving y free.  (This is not exactly the "spring force" that @theahura seems to want). A pre-alpha, simple working constraint ensures that all non-anchors remain between my best/worst x limits.
BTW, another issue (even in #620) is that UMAP init phase applies dimension-wise scale factors
even for init being an ndarray.

If I init with a previous embedding ndarray, for example, with carefully set "euclidean" distance, I don't like UMAP rescaling as if I suddenly wanted a weighted-euclidean embedding for the init!
If I want to anchor some points in my init ndarray, and use gradient masking in a constraint, they do end up anchored ... but "somewhere else".  (Is this historical cruft? Didn't spectral init just do its own rescaling?)

Now, when constraints come into play, init becomes a little more complex.  I'm thinking some types of constraint objects may add a function that can approximately satisfy a constraint.  Some constraints that put more load on layouts.py iterations might reasonably provide some rotate/(scale?)/translate of init data to ease the load.


Fix visibility setting to ViewVisibility

Hello!
In the migration to 0.12 in #43, there was a mistake here where a ComputedVisibility.set_visible_in_view() was migrated to a setting to InheritedVisibility.
This resulted in the plugin breaking all hierarchical visibility propagations as soon as a grid is spawned, making everything always visible at all times.
In this PR I changed it to what it should have been migrated to, which is a setting to ViewVisibility.
CC @pcwalton  just for a sanity check

Thank god, tracking down that it was this crate rather than an error in my code took me ages to find!

LGTM

Bumped the patch version!

Thank god, tracking down that it was this crate rather than an error in my code took me ages to find!

I hear you! It took me several days, a plea for help in Discord and digging all the way into bevy_hierarchy to finally figure it out, it really was a journey

Welp, looks like bumping from a branch of someone that isn't an owner of the crate doesn't work with our CI. I'll revert the commit and bump it myself. Sorry about that.

Thanks for the quick review! Can you folks push a patch release to crates.io? I would almost consider yanking the previous version since the bug is pretty severe but I'll leave the choice up to you!

Hey, very sorry about that, we had CI issues and I never realized that a version with this fix was never published. I just published it so now 0.10.1 has the fix and is compatible with bevy 0.12.
In the bevy 0.13 version of this crate we just removed the shadow feature because it was causing too many issues like this.


NTR: axonemal basal plate assembly

Hi,
Can I request a GO term for axonemal basal plate assembly please?
Accession: GO:xxxxxx
Name: axonemal basal plate assembly
Ontology: biological_process
Synonyms: axonemal basal plate formation, axoneme basal plate assembly, basal plate assembly
Definition: The aggregation, arrangement and bonding together of a set of components to form an axonemal basal plate.
is_a: GO:0035082! axoneme assembly
Source: GO:0097541, PMID:23352055, PMID:30810527
Thanks & best wishes,
Achchuthan

This won't be

is_a: GO:0035082! axoneme assembly

because the basal plate isn't a type of axoneme, but rather a part_of axoneme assembly

Hi @krchristie
Thanks for your correction. It makes sense to me.
Best wishes,
Achchuthan


Install fails with Python 3.11

Installing python package doesnt work in clean environment with python 3.11 because of issue with pyarrow.
I'm not super familiar with how poetry works but I didnt see pyarrow as explicit dependency, so might be worth limiting to less than python 3.11 for now or forcing newer versions of pyarrow
To repro
conda create -n zenotest python
conda activate zenotest
pip install zenoml

Fails with weird issue for pyarrow:
Failed to build pyarrow
ERROR: Could not build wheels for pyarrow, which is required to install pyproject.toml-based projects

However if environment is created with python 3.10 explicitly then works fine
conda create -n zenotest python=3.10
conda activate zenotest
pip install zenoml

Apparently had it set to not support 3.11 so it was installing an old version that required pyarrow that did not work for 3.11. Anyway thanks for the find, should be fixed now.


Releases aren't tagged

As far as I can tell, there isn't a way to download a source tarball of a given version of this extension. There aren't any Git tags or GitHub releases. Would it be possible to push a git tag of each release going forward?

Very late reply (sorry), but yes - we can begin doing that moving forward.
Thank you for the suggestion.


Mobius REPL

[Current coverage][cc-pull] is 66.90% (diff: 100%)

Merging [#508][cc-pull] into [master][cc-base-branch] will decrease coverage by 14.69%

@@             master       #508   diff @@
==========================================
  Files            61          2     -59
  Lines          6869        278   -6591
  Methods        1121          0   -1121
  Messages          0          0
  Branches        883          0    -883
==========================================
- Hits           5605        186   -5419
+ Misses          890         88    -802
+ Partials        374          4    -370

Powered by Codecov. Last update [9dc4674...7e879e1][cc-compare]
[cc-base-branch]: https://codecov.io/gh/Microsoft/Mobius/branch/master?src=pr
[cc-compare]: https://codecov.io/gh/Microsoft/Mobius/compare/9dc4674e93b216d29a22ec2b5c060a556c3442d0...7e879e118054e277ea5c009129c64e5db8b09283?src=pr
[cc-pull]: https://codecov.io/gh/Microsoft/Mobius/pull/508?src=pr

@tawan0109 - can you send a CR request in CodeFlow as well?

@skaarthik
Sure, will send out a CR.


techdocs-backend: fix http mock in cacheMiddleware test

Seems a dep bump has broken these tests because of missing carriage returns in the HTTP response.

Looks like this was due to a Node.js version bump, the recent release has more strict HTTP parsing: https://nodejs.org/en/blog/release/v14.20.0/


日志最好有轮滚，避免出现把磁盘写满的情况

参考
https://github.com/clusterpedia-io/clusterpedia/blob/7e301c8ce4cf81827850ab0f58f64b0457563f76/pkg/storage/internalstorage/register.go#L87

Although the internalstorage will only print logs of errors and Slow SQL by default, there is still a risk of oversizing the log file in some cases.
It will be added to the roadmap


message-relayer supplemental development

The message-relayer is almost developed, but its functionality on the private-opstack hasn't been confirmed yet. Therefore, we need to ensure that it operates correctly on the private-opstack. I believe some additional development may be required.
What is message Relayer
The message relayer is a service that facilitates the relaying of transactions from L2 to L1. When a user initiates the withdrawal process, the subsequent steps are automatically handled by the relayer.
Referring to the bridge tutorial, the withdrawal process is outlined in this section. Looking at the code, steps beyond step 3 are managed by the relayer, specifically, the proveMessage and finalizeMessage functions. Therefore, what users need to do manually is only execute the withdrawETH function.
The previous version can be found here.
Repo
message-relayer
this is my personal repo, thought please arrange PR to this repo.

Batch Finalization of Transactions in L2 to L1 Bridge
The process of transferring transactions from Layer 2 (L2) to Layer 1 (L1) typically involves two distinct steps:

the integrity of the withdrawal transaction from L2 is verified on L1. This step ensures that the transaction is valid and consistent with L2's state.

https://github.com/oasysgames/private-opstack/blob/main/bridge-tutorial/src/withdraw-oas.ts#L72

Next, the withdrawal from L2 is finalized on L1. This step completes the transaction, officially recording it on the L1.

https://github.com/oasysgames/private-opstack/blob/main/bridge-tutorial/src/withdraw-oas.ts#L106

A message-relayer is responsible for performing these steps on behalf of users. To improve efficiency, the message-relayer employs a technique known as multicalling. Multicalling consolidates multiple function calls into a single call. This approach reduces the overhead and complexity of processing each transaction individually, leading to more streamlined operations.
https://github.com/makerdao/multicall/blob/16ec5e2859b3a4829ceed4ee1ef609e6e9a744ee/src/Multicall2.sol#L55
The task here is altering the implementation of the finalization call.
Presently, the finalize function is called through a multicall. However, the plan is to transition this process to a batch calling method(developing now)
We redesign the process now finalize function can only be executed by the message-relayer. As such, the modification in the finalization process involves replacing the existing multicall approach with the new batch call method, adhering to the protocol that only the message-relayer can initiate this process.


Does not produce same results via curl API for the same model.

What is the issue?
export OLLAMA_HOST="<IP_ADDRESS>:3336"; ollama create tagger -f tagger_Modelfile && ollama run tagger
Running the below does NOT produce the same result as in the terminal cli in the above command.
curl http://localhost:3336/api/generate -d '{
  "model": "tagger",
  "prompt": "hello"
}'

with or without streaming.
It seems like it is using a different model somehow, it just is not giving the same responses at all.
tagger_Modelfile:
FROM gemma:7b
PARAMETER temperature 0.5
PARAMETER num_ctx 8192

TEMPLATE """<|im_start|>system
{{ .System }}<|im_end|>
<|im_start|>User
{{ .Prompt }}<|im_end|>
<|im_start|>Assistant
"""

SYSTEM """
Categorize user text using hierarchical tags.
You are to respond in one sentence. Example responses:
- #mathematics #linear-algebra #matrices #vectors
- #philosophy #epistemology
- #computer-science #algorithms #memoization
- #statistics #probability-theory
- #language #grammar
- #statistics #sample-theory #confidence-intervals
Especially important to get down whether it is calculus, analysis, combinatorics, etc.
"""
PARAMETER stop "<|im_start|>"
PARAMETER stop "<|im_end|>"

MESSAGE user """
Matrix, a set of numbers arranged in rows and columns so as to form a rectangular array. The numbers are called the elements, or entries, of the matrix. Matrices have wide applications in engineering, physics, economics, and statistics as well as in various branches of mathematics.
"""
MESSAGE assistant #mathematics #linear-algebra #matrices
MESSAGE user """
the binomial coefficients are the positive integers that occur as coefficients in the binomial theorem. Commonly, a binomial coefficient is indexed by a pair of integers n ≥ k ≥ 0
"""
MESSAGE assistant #mathematics #combinatorics #binomial-coefficient

Help much appreciated!
OS
Linux
GPU
Nvidia
CPU
Intel
Ollama version
0.1.32

Hi @MathematicianOnGithub Models don't give the same answer each time, specially for an open prompt like "Hello".
If you want answers to look very close the can set the temperature to 0.
Do you notice a bigger difference as if you use twice the same prompt without API?

Hi @igorschlum
Yes I tried using the same prompt 20 times out of 20 in the CLI REPL, I get expected response even after restarting.
Through the API 20 out of 20 observations I don't get expected response. Same when I changed the temperature.
So there is indeed a statistical significance here. I was up testing and trying stuff for 4 hours yesterday night, but to no avail.
I also listed the model through the API endpoint to verify, I also tried using "tagger:latest" as the model name which seemed more consistent with its name, but still to no avail.
I also tried different prompts of course, still to no avail.

Make sure you specify a seed, so random generator use the same seed every time.

I made an assumption that their cli uses http as well, so I used tcpdump, and then it is starting to make sense:
E<EMAIL_ADDRESS>..#-.-..POST /api/chat HTTP/1.1
Host: <IP_ADDRESS>:3336
User-Agent: ollama/0.1.32 (amd64 linux) Go/go1.22.2
Content-Length: 776
Accept: application/x-ndjson
Content-Type: application/json
Accept-Encoding: gzip
{"model":"tagger","messages":[{"role":"user","content":"\nMatrix, a set of numbers arranged in rows and columns so as to form a rectangular array. The numbers are called the elements, or entries, of the matrix. Matrices have wide applications in engineering, physics, economics, and statistics as well as in various branches of mathematics.\n"},{"role":"assistant","content":"#mathematics #linear-algebra #matrices"},{"role":"user","content":"\nthe binomial coefficients are the positive integers that occur as coefficients in the binomial theorem. Commonly, a binomial coefficient is indexed by a pair of integers n ... k ... 0\n"},{"role":"assistant","content":"#mathematics #combinatorics #binomial-coefficient"},{"role":"user","content":"hello"}],"format":"","options":{}}
It seems to be sending multiple requests along with the "messages", so basically the CLI is not 1:1 with the curl API.
but at least now I understand a little bit more how it works.


Generate padrino rake tasks instead of loading them in.

I think it would be better if the component specific rake tasks were generated into an app instead of loaded in. This allows users to modify them to whatever their needs be. What do you guys think? Example:
$ padrino g project foo -d mongoid

which generates something like maybe foo/lib/tasks/mongoid.rake? Thoughts? @nesquena @DAddYE @skade @joshbuddy @nu7hatch?

My first idea was that, In my previous works like lipsiadmin I used that, but the problem is when we found a bug or something wrong we need to fix by hands each project, then we have extra code in each app and like for AR we didn't touch so much these tasks.

What do you think if like Rakefile we allow user to deep copy our tasks from our gem if that fits their needs?
$ padrino g rakefile --all

only rakefile generates the current Rakefile, with --all includes also custom orm tasks. Thoughts?


Remove glob from the standard library

The glob package is being removed from the standard library and
moved to a new home at https://github.com/ponylang/glob/ where it
will live on as an independent library.
It is being removed because it has a transitive dependency on an
external library libpcre and that dependency makes creating release
artifacts more difficult.
At the moment we have to deal with packaging up pcre for each Linux
distro etc and they all have their own methods to do so. This
lead us to do a lot of work on supporting distro specific packaging.
That has turned out to be too much work. We are moving to having
a single glibc Linux friendly .tar.gz that can be done to install
Pony.
To faciliate this move, we decided that we want to remove items from
the standard library that depend on external libraries like pcre.
Full conversation about the decision is available in the audio of
the Pony development sync July 9, 2019 audio that you can download
from: https://sync-recordings.ponylang.io/r/2019_07_09.m4a

I'm going to verify this passes CI then squash and merge.


init storage hooks when starting chat modules

prevents a deadlock if a hook is trying to be added during login/logout

(ci flake unrelated)


[Problems panel] "Show Active File Only" does not work when a folder is selected

Does this issue occur when all extensions are disabled?: Yes

VS Code Version: 1.59.1
OS Version: Windwos_NT x64 10.0.19043

Steps to Reproduce:

Open a workspace that has a lot of errors
Open the Problems panel and enable the filtering option "Show Active File Only"
Click on a File in the Explorer:  the panel is refreshed and only the errors/warnings for that file are shown
Click on a Folder in the Explorer: the panel is not refreshed and the same errors/warnings are shown

I was expecting that this would work the same as what I'm used to with Eclipse, which helps drilling down when you have an "interesting" legacy application to improve, with thousands errros/warnings...
Also, this is even more helpful for workspaces having multiple projects (folders ?) in them, because sometimes quality varies from one project to another, and I did not find a way to temporarily disable an entire project from the problems tab (some people had similar need if I understand right)

Filter Show Active File Only shows problems for the file that is opened and active in the editor. It is not for folders. You can use text/glob filter input to filter by folders


pip install error

bogon:~ hubin$ pip install android-resource-remover
Collecting android-resource-remover
Using cached android-resource-remover-0.1.5.tar.gz
Requirement already satisfied (use --upgrade to upgrade): lxml>=3.3.3 in /Library/Python/2.7/site-packages (from android-resource-remover)
Installing collected packages: android-resource-remover
Running setup.py install for android-resource-remover
Complete output from command /usr/bin/python -c "import setuptools, tokenize;file='/private/var/folders/t0/sl2174ps6dq7__dr4cbvrm7h0000gn/T/pip-build-IAYg_g/android-resource-remover/setup.py';exec(compile(getattr(tokenize, 'open', open)(file).read().replace('\r\n', '\n'), file, 'exec'))" install --record /var/folders/t0/sl2174ps6dq7__dr4cbvrm7h0000gn/T/pip-9aRlIK-record/install-record.txt --single-version-externally-managed --compile:
running install
running build
running build_py
creating build
creating build/lib
copying android_clean_app.py -> build/lib
running install_lib
copying build/lib/android_clean_app.py -> /Library/Python/2.7/site-packages
error: could not delete '/Library/Python/2.7/site-packages/android_clean_app.py': Permission denied
----------------------------------------

Command "/usr/bin/python -c "import setuptools, tokenize;file='/private/var/folders/t0/sl2174ps6dq7__dr4cbvrm7h0000gn/T/pip-build-IAYg_g/android-resource-remover/setup.py';exec(compile(getattr(tokenize, 'open', open)(file).read().replace('\r\n', '\n'), file, 'exec'))" install --record /var/folders/t0/sl2174ps6dq7__dr4cbvrm7h0000gn/T/pip-9aRlIK-record/install-record.txt --single-version-externally-managed --compile" failed with error code 1 in /private/var/folders/t0/sl2174ps6dq7__dr4cbvrm7h0000gn/T/pip-build-IAYg_g/android-resource-remover

bogon:~ hubin$ sudo pip install android-resource-remover
Password:
The directory '/Users/hubin/Library/Caches/pip/http' or its parent directory is not owned by the current user and the cache has been disabled. Please check the permissions and owner of that directory. If executing pip with sudo, you may want sudo's -H flag.
The directory '/Users/hubin/Library/Caches/pip' or its parent directory is not owned by the current user and caching wheels has been disabled. check the permissions and owner of that directory. If executing pip with sudo, you may want sudo's -H flag.
Collecting android-resource-remover
Downloading android-resource-remover-0.1.5.tar.gz
Requirement already satisfied (use --upgrade to upgrade): lxml>=3.3.3 in /Library/Python/2.7/site-packages (from android-resource-remover)
Installing collected packages: android-resource-remover
Running setup.py install for android-resource-remover
Complete output from command /usr/bin/python -c "import setuptools, tokenize;file='/private/tmp/pip-build-Tegqhi/android-resource-remover/setup.py';exec(compile(getattr(tokenize, 'open', open)(file).read().replace('\r\n', '\n'), file, 'exec'))" install --record /tmp/pip-bC4yPh-record/install-record.txt --single-version-externally-managed --compile:
running install
running build
running build_py
creating build
creating build/lib
copying android_clean_app.py -> build/lib
running install_lib
copying build/lib/android_clean_app.py -> /Library/Python/2.7/site-packages
byte-compiling /Library/Python/2.7/site-packages/android_clean_app.py to android_clean_app.pyc
running install_data
copying AUTHORS -> /System/Library/Frameworks/Python.framework/Versions/2.7/.
error: [Errno 1] Operation not permitted: '/System/Library/Frameworks/Python.framework/Versions/2.7/./AUTHORS'
----------------------------------------

Command "/usr/bin/python -c "import setuptools, tokenize;file='/private/tmp/pip-build-Tegqhi/android-resource-remover/setup.py';exec(compile(getattr(tokenize, 'open', open)(file).read().replace('\r\n', '\n'), file, 'exec'))" install --record /tmp/pip-bC4yPh-record/install-record.txt --single-version-externally-managed --compile" failed with error code 1 in /private/tmp/pip-build-Tegqhi/android-resource-remover

seems a problem with your permissions. try installing it in virtual env


RATIS-1318. Remove incubating

What changes were proposed in this pull request?
Remove incubating
What is the link to the Apache JIRA
https://issues.apache.org/jira/browse/RATIS-1318
How was this patch tested?
no need new ut.

@runzhiwang , thanks a lot for working on this.  There are a few other "incubator" or "incubating" found in make_rc.sh.
{code}
-- ./dev-support/make_rc.sh ---------------------------------------------------
82:   svn co https://dist.apache.org/repos/dist/dev/incubator/ratis "$SVNDISTDIR"
119:   tar zvxf "$projectdir/ratis-assembly/target/apache-ratis-incubating-${RATISVERSION}-src.tar.gz"
120:   cd "apache-ratis-incubating-${RATISVERSION}"
130:   cp "$WORKINGDIR/apache-ratis-incubating-${RATISVERSION}/ratis-assembly/target/apache-ratis-incubating-${RATISVERSION}-bin.tar.gz" "apache-ratis-incubating-${RATISVERSION}-bin.tar.gz"
131:   cp "$projectdir/ratis-assembly/target/apache-ratis-incubating-${RATISVERSION}-src.tar.gz" "apache-ratis-incubating-${RATISVERSION}-src.tar.gz"
182:    10. (If the vote passed): Send out the next voting mail to the incubator mailing list.
{code}

-- ./dev-support/make_rc.sh ---------------------------------------------------
 82:   svn co https://dist.apache.org/repos/dist/dev/incubator/ratis "$SVNDISTDIR"
119:   tar zvxf "$projectdir/ratis-assembly/target/apache-ratis-incubating-${RATISVERSION}-src.tar.gz"
120:   cd "apache-ratis-incubating-${RATISVERSION}"
130:   cp "$WORKINGDIR/apache-ratis-incubating-${RATISVERSION}/ratis-assembly/target/apache-ratis-incubating-${RATISVERSION}-bin.tar.gz" "apache-ratis-incubating-${RATISVERSION}-bin.tar.gz"
131:   cp "$projectdir/ratis-assembly/target/apache-ratis-incubating-${RATISVERSION}-src.tar.gz" "apache-ratis-incubating-${RATISVERSION}-src.tar.gz"
182:    10. (If the vote passed): Send out the next voting mail to the incubator mailing list.

@szetszwo  Hi, line 119, 120, 130, 131 already changed in this PR. line 82 need to change dir, if we remove incubator, the dir will be https://dist.apache.org/repos/dist/dev/ratis, which does not exist.

@runzhiwang , I just have created https://dist.apache.org/repos/dist/dev/ratis/  and copied KEYS to there.

I just have created https://dist.apache.org/repos/dist/dev/ratis/ and copied KEYS to there.

@szetszwo Thanks, do we put release 2.0.0 to https://dist.apache.org/repos/dist/dev/ratis/? and do we need to copy the previous release such as 1.0.0 to https://dist.apache.org/repos/dist/dev/ratis/?

Yes, we should put the 2.0.0 release to the new dir.  For the old releases, we will move them once we have fixed the links in the web pages.

@szetszwo Hi, I have updated the patch, there are other "incubator" and "incubating" related to repository name and email, so I did not change them.


[HHH-10588] use H2Dialect in ConnectionsReleaseTest

https://hibernate.atlassian.net/browse/HHH-10588

Applied on master, 5.1, and 5.0. Thanks for the fix.


Change List to scala.Seq in trees

A recent refactoring changed all occurrences of immutable.Seq to List in both syntactic and semantic API. However, we quickly figured that this may not be good enough for Database, so we changed Database.entries from List to scala.Seq.
I propose that we make the same change to trees, too. Previous discussion: https://github.com/scalameta/scalameta/pull/907#issuecomment-306210194. In addition to all those arguments in favor of scala.Seq, we now have an argument of consistency.

The main argument I hear against Seq is that it isn’t immutable by default but the strawman collections proposal has Seq defaulting to be immutable (tentatively scheduled for 2.13) in which case the original complaint may not last that much longer.

I am not sure we need so much consistency in our collection choices for unrelated data structures across modules. I think it's fine to use List on trees and Seq in Database. Tokens already use arrays, and for good reasons. Data structures have different shapes and requirements. My experience is that

databases can become large (>30.000 elements)
the surface code I write against database is quite small (load + dump)

Trees are used differently

each List is almost always small
the surface code I write against trees is large (repl, rewrites, macros)

Here's my opinion.
The entire scalameta tree hierarchy must retain immutability, otherwise no consumer of the scalameta api can reason about the internals of scalameta. This requires all fields to have some immutable.Seq type.
If we allow inputs of type scala.Seq/ we immediately have to copy that to an immutable.Seq of some kind unless it is already an immutable.Seq.
@ShaneDelmore Correct me if I am wrong, but I was under the impression that scala.Seq's apply method was changing, not that scala.Seq's api was changing, thus if you will still be able to have a scala.Seq that is mutable.
In regards to consistency, I don't think collection types should be decided because of consistency. As @olafurpg points out, the semantic database is a completely separate api with it's own needs. List is a great choice for Tree's
We could definitely add setters to Tree fields that are of type List, so that we can create Tree subtypes with scala.Seq. We just would need to defensively copy anything that's not an immutable.Seq.

@DavidDudson I was mistaken, there is only a suggestion to make the strawman Seq immutable.
https://github.com/scala/collection-strawman/issues/149
I upvoted this based on the thinking that scala Seq was moving towards immutable, if that doesn’t end up happening then I agree I would prefer List to have the immutability guarantee.

Allright, let's keep lists in trees.
Regarding List becoming Seq in Database. I accepted that PR (see https://github.com/scalameta/scalameta/issues/996 for details) when I just woke up and soon enough started regretting that decision.
My reason for regret is that the only argument provided in favor of the change was performance-related, but it wasn't accompanied by benchmark results. Our experience with scalac taught me that gut feeling doesn't always work well in the matters of performance, so we should've waited for concrete numbers.
I don't want to make any more hasty decisions, so let's keep the status quo, but let's see whether Lists are as bad as they are touted to be. I've opened a ticket to investigate that: https://github.com/scalameta/scalameta/issues/1012.


Prototype vite env integration

Addresses https://github.com/Effect-TS/effect/issues/1498

Wont't work unfortunately due to https://vitejs.dev/guide/env-and-mode.html#production-replacement


Quick setup instructions missing directory creation

In the Quick Setup documentation it should probably say:
$ git clone git@github.com:lens-protocol/core.git lens-protocol
because the next step assumes that this is the directory where the clone was created.

yep! I have also faced this, because in next step they suggest cd lens-protocol.
and git clone into core folder.
it may be cd core in next step

cd core instead

Agreed with updating the dev docs.

Docs updated https://github.com/lens-protocol/core?tab=readme-ov-file#1-clone-the-repository


test(backends): enable tests on different backends

enable unit tests on different backends

backends testing env setup
enable unit tests on different backends
add this to CI

Seems like a good idea. I think it would also be a good idea to publish a step support matrix to the website, as it's hard to work around a step that contains operations that aren't supported on your backend (more so than on the core Ibis repo, where you may be able to drop into raw SQL or find some workaround), because step definitions are broader in scope. As a result, e.g. if somebody wants to use the TargetEncode step, they can first check whether it's supported on their backend.

Two more things to think about:

Can we make the step support matrix without actually having to connect to backends in the CI? E.g. if quantile operation isn't supported on a backend, can we catch the would-be failure in the step definition without actually having to connect to an actual backend?
Does it make sense to do this as unit tests, or as something higher-level (like BDD)?
If this is a big task, should we prioritize a few backends first? Which ones?

Feedback:

You can compile expressions without a connection (using ibis.to_sql and specify the dialect), and you should also be able to compile without any dependencies.

If you want to do execution testing (may not be necessary?):

Start with 2 backends—DuckDB and something else (probably not BigQuery, too slow to iterate rapidly upon in a testing setup). Maybe pick Clickhouse as the second (differs from DuckDB on scale, default nullability behavior, function naming, etc.); something like Postgres is too similar to DuckDB in terms of SQL.


Add options for always showing the cursor and an aiming offset.

In game options for customizing where on the screen the cursor is locked to when holding right click or while in action mode.

Toggle for whether to always show mouse cursor.

Cheers

Added in v1.4.0


IE9 fails if developer console is not opened

We are using hwcrypto 0.0.9 and hwcrypto-legacy 0.0.9.
When using IE9 to for signing, it all works great if the developer console (F12) is open. However, if a signing session is started without the console being open, the signing fails with the error "Unable to get value of the property 'getCertificate': object is null or undefined".
A similar issue can be observed at the test site https://open-eid.github.io/hwcrypto.js/sign.html, where the property 'use' is null or undefined.
Is this a know issue?

Wow, this sounds like a nice thing to debug :)
No, this is not a known issue, it has been tested with older IE-s only via the compatibility mode.
If you open the console AFTER the signing fails, does IE9 show any past messages ?

If I open the console after the signing fails, no log messages are displayed.
However, if I first call getCertificate without having the console open, then open the console, and then call getCertificate once more you can see the new messages.

Okay, turns out that IE8/9 only define console.* when devtools is open. Yet another reason to remove them from released code, available in a few minutes.


rosa login fails on Windows 10 crypto/x509: system root pool is not available on Windows

The command rosa login fails using Windows 10.
C:\> rosa login --token="<<HIDDEN>>"
ERR: Failed to create OCM connection: crypto/x509: system root pool is not available on Windows

Fixed by https://github.com/openshift/rosa/pull/228


SRS Review

invite @robi-y
move srs doc to docs folder
missing main scenario for use-cases

https://github.com/YonaMilstein/QUALITA/wiki/SRS

Let's go over it on Sunday

went over it. done


Add intention to award dates

These dates are needed on the framework dashboard.
The timezones have been added as markup and a spike added to the icebox (#109431100) to review how dates are managed

Only point is I'd say this should be 0.13.0, not 0.12.2 as it's a feature you're adding here, not a bug fix.


fix(language-server): fix panic by building scope tree child ids

closes #7434

#7440  👈 (View in Graphite)
main

This stack of pull requests is managed by Graphite. Learn more about stacking.


Permission property on AccessPolicy model should be called "Permissions"

This should be done in the transform for now.


Share icons

Social share icons should be enabled, and that should be customizalbe(on/off).

fixed in 68a2a3f, but not confirmed in public server(fb share needs to confirm in public server).

Closed. I will let it reopen when not fixed in public server.


Replace reth ReceiptWithBloom type with alloy's ReceiptWithBloom

Describe the feature
in reth we have
https://github.com/paradigmxyz/reth/blob/3b120283192f276562de4f9019e6c3b59dc1efc4/crates/primitives/src/receipt.rs#L196-L201
in alloy we have almost the identical type:
https://github.com/alloy-rs/alloy/blob/b959ea621453d4b4a953b9d04e21faffc921b127/crates/consensus/src/receipt/receipts.rs#L125-L131
we can't easily unify those just yet because alloy's type is generic over logs, we first need to change alloy's type to be generic over receipt and change the default to T = Receipt<Log>
so this issue is two-fold,

unblock via changes on alloy
migrate reth to alloy's type

Additional context
No response

Would love to take this one @mattsse

I’d like to work on this.

I’d like to work on this.

Hi, I am already half way through with two prs merged for this on alloy and op-alloy. Will open the final pr today.

I’d like to work on this.

Hi, I am already half way through with two prs merged for this on alloy and op-alloy. Will open the final pr today.


Is there any way we can integrate Acuity Booking Schedular or Google Calendar Sync to this package?

Hey, thanks for the suggestion! These integrations would definitely be cool additions to the package.
Adding Acuity Booking Scheduler or Google Calendar Sync is totally doable (not familiar with Acuity Booking, though), but it's not on my immediate to-do list. I'm juggling a few other priorities right now, so it might take some time before I can get to it.
If you're handy with code and know how to implement these integrations, I'd love to see a pull request and would help to code it for sure! That'd be the quickest way to get these features up and running.
If coding's not your thing, no worries at all. I've added your ideas to my feature wishlist. I can't promise a super quick turnaround, but they're definitely not off the table for the future.
Got any specific use cases in mind for these integrations? I'd be interested to hear more about how you're thinking of using them.
Thanks again for the input – it's great to hear ideas for improving the package!

Hi @Junaidiqbal35, see my PR #265


Rework autocompletion to add parentheses to function calls

Won't be implemented by Gleam's LSP: https://github.com/gleam-lang/gleam/issues/3674
Would be interesting to look into PSI context-dependant addition of parentheses using LSP4IJ's v0.7.0 LSP*Feature customization.


Remove test for legacy MiqReport

Removed special handling of legacy MiqReport while importing

Do we just not support legacy reports anymore via upgrade?  Does it make sense to just have a migration to ensure this?  (I'm not even sure how old this is...if it's older than, C-release I think (whatever the version you are forced to upgrade to), then this is probably ok.
cc @gtanzillo ?

This commit 7c78517f3e2 is from 2013 via @lfu
I do remember running into this scenario years back, but can't place why.
Think it was a customer who had a yaml file with a number of reports in it.
Think maybe they were exporting the  "shame" report?
(Sorry, not trying to be vague here. I just remember enjoying the name of the report. Of course the details elude me)

@Fryguy @kbrock what should we do with this PR?

Waiting on response from @gtanzillo

To be honest, I'm not familiar with the issue that the "legacy report" check was meant to address. I do recall that in the distant past we had an issue with ActiveRecord objects that were serialized in report results and needed some special code to deal with then when the internal AR object format was changed. But this is in the report definition.

The only concern I have is when we export a bunch of miq_reports in a single yaml file. I thought this was needed to import it back again.
That is the only use case I know of. I don't know how to export or import them, I just know we had this functionality within the past few years.
If that still works then I'm :+1:


Re-enabling Sonar Scans

Re-enabling sonar scans for this repo.
https://github.com/open-cluster-management/backlog/issues/10316

:tada: This PR is included in version 2.0.11 :tada:
The release is available on GitHub release
Your semantic-release bot :package::rocket:


Avro serializer fails to deserialize a Dictionary<TKey, TValue> with more then 1026 KeyValuePairs.

Here is a minimal, complete reproduce of the problem:
void Main()
{
    Dictionary<int, int> dsi = new Dictionary<int, int>();
    for (int i = 0; i < 1027; i++)
    {
     dsi.Add(i, i);
    }

    var serializer = AvroSerializer.Create<Dictionary<int, int>>();
    var ms = new MemoryStream();
    serializer.Serialize(ms, dsi);
    ms.Seek(0, SeekOrigin.Begin);
    var result = serializer.Deserialize(ms);
}

Basically, when the dictionary has more than 1024 values, we get a SerializationException with the error message:
"Invalid integer value in the input stream."
When trying to deserialize the stream. I'm assuming this has something to do with the memory optimization performed by the EnumerableSerializer.

@YuvalItzchakov please open a new issue if the problem still exists/repros.


InResponseToField of the Response doesn't correspond to sent message | SP - 2.6.0

Hello,
I'm encountering a strange variant of SAMLException
I'm getting this error
e.o.containerproxy.service.UserService   : Authentication failure [user: ] [error: Error validating SAML message]
org.opensaml.common.SAMLException: InResponseToField of the Response doesn't correspond to sent message XXXXXX
Error is the same as in the case of:
https://github.com/openanalytics/shinyproxy/issues/335
I tried to solve it using the suggested procedure in the documentation
server:
  secure-cookies: true
proxy:
  same-site-cookie: None

The problem is that if I run the application in Safari or Firefox without using the above configuration login works as it should. But it doesn't work in Chrome.
If I add the config, the login works in Chrome but not in Safari and Firefox.
ShinyProxy version - 2.6.0
SAML in YML
  saml:
    idp-metadata-url: https://XXXXXX.eu.auth0.com/samlp/metadata/XXXXXX
    app-entity-id: urn:XXXXXX.eu.auth0.com
    app-base-url: http://localhost:8080
    name-attribute: http://schemas.xmlsoap.org/ws/2005/05/identity/claims/emailaddress
    roles-attribute: http://schemas.auth0.com/roles
    logout-url: https://XXXXXX.eu.auth0.com/v2/logout?client_id=XXXXXX&returnTo=http://localhost:8080
    nameidentifier-attribute: http://schemas.xmlsoap.org/ws/2005/05/identity/claims/nameidentifier
    email-verified-attribute: http://schemas.auth0.com/email_verified
    created-at-attribute: http://schemas.auth0.com/created_at
    lb-server-name: localhost:8080
    lb-scheme: http

Hi
Can you check the following things?

are you accessing ShinyProxy using localhost:8080? If so, you could try using a proper domain name. If not you will have to updat ehte app-base-url property.
are you using HTTPS? The secure-cookies property requires you to use HTTPS. Usually if using localhost, HTTPS is not required but this may differ between browsers.

Hello,
localhost:8080 is just for dev version. on the production version we use https app-base-url: https://app.xxx.xx
and there was the same problem with incompatibility of certain browsers.

Hi
Thanks for reporting back! Since this issue is fixed, I'm going to close it. Feel free to open a new issue if you encounter any problem.


Multiple users are able to sign up with the same email

The email that users can use for sign-up does not have a unique check and multiple users are able to sign in using the same Email Id.

@bjarneo Can I work on adding a unique check to the emailId field so that multiple users cannot use the same email id?


add node id to pageserver

This adds node id parameter to pageserver configuration. Also I use a
simple builder to construct pageserver config struct to avoid setting
node id to some temporary invalid value. Some of the changes in test
fixtures are needed to split init and start operations for envrionment.

Let's also add  -c "id='10'" to docker-entrypoint.sh for console development/testing.


ActiveRecord::PendingMigrationError:
Migrations are pending. To resolve this issue, run:
bin/rake db:migrate RAILS_ENV=development

View details in Rollbar: https://rollbar.com/trystant/BOW/items/284/

ActiveRecord::PendingMigrationError:

Migrations are pending. To resolve this issue, run:

	bin/rake db:migrate RAILS_ENV=development

  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/activerecord-<IP_ADDRESS>/lib/active_record/migration.rb", line 392, in check_pending!
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/activerecord-<IP_ADDRESS>/lib/active_record/migration.rb", line 373, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/actionpack-<IP_ADDRESS>/lib/action_dispatch/middleware/callbacks.rb", line 29, in block in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/activesupport-<IP_ADDRESS>/lib/active_support/callbacks.rb", line 88, in __run_callbacks__
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/activesupport-<IP_ADDRESS>/lib/active_support/callbacks.rb", line 778, in _run_call_callbacks
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/activesupport-<IP_ADDRESS>/lib/active_support/callbacks.rb", line 81, in run_callbacks
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/actionpack-<IP_ADDRESS>/lib/action_dispatch/middleware/callbacks.rb", line 27, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/actionpack-<IP_ADDRESS>/lib/action_dispatch/middleware/reloader.rb", line 73, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/actionpack-<IP_ADDRESS>/lib/action_dispatch/middleware/remote_ip.rb", line 78, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/rollbar-2.2.1/lib/rollbar/middleware/rails/rollbar.rb", line 24, in block in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/rollbar-2.2.1/lib/rollbar.rb", line 837, in scoped
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/rollbar-2.2.1/lib/rollbar/middleware/rails/rollbar.rb", line 22, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/actionpack-<IP_ADDRESS>/lib/action_dispatch/middleware/debug_exceptions.rb", line 17, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/rollbar-2.2.1/lib/rollbar/middleware/rails/show_exceptions.rb", line 22, in call_with_rollbar
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/web-console-2.1.2/lib/web_console/middleware.rb", line 37, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/actionpack-<IP_ADDRESS>/lib/action_dispatch/middleware/show_exceptions.rb", line 30, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/railties-<IP_ADDRESS>/lib/rails/rack/logger.rb", line 38, in call_app
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/railties-<IP_ADDRESS>/lib/rails/rack/logger.rb", line 20, in block in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/activesupport-<IP_ADDRESS>/lib/active_support/tagged_logging.rb", line 68, in block in tagged
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/activesupport-<IP_ADDRESS>/lib/active_support/tagged_logging.rb", line 26, in tagged
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/activesupport-<IP_ADDRESS>/lib/active_support/tagged_logging.rb", line 68, in tagged
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/railties-<IP_ADDRESS>/lib/rails/rack/logger.rb", line 20, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/ahoy_matey-1.1.1/lib/ahoy/engine.rb", line 20, in call_with_quiet_ahoy
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/request_store-1.1.0/lib/request_store/middleware.rb", line 8, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/actionpack-<IP_ADDRESS>/lib/action_dispatch/middleware/request_id.rb", line 21, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/rack-1.6.4/lib/rack/methodoverride.rb", line 22, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/rack-1.6.4/lib/rack/runtime.rb", line 18, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/activesupport-<IP_ADDRESS>/lib/active_support/cache/strategy/local_cache_middleware.rb", line 28, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/rack-1.6.4/lib/rack/lock.rb", line 17, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/actionpack-<IP_ADDRESS>/lib/action_dispatch/middleware/static.rb", line 116, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/rack-1.6.4/lib/rack/sendfile.rb", line 113, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/railties-<IP_ADDRESS>/lib/rails/engine.rb", line 518, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/railties-<IP_ADDRESS>/lib/rails/application.rb", line 165, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/rack-1.6.4/lib/rack/content_length.rb", line 15, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/puma-2.11.2/lib/puma/server.rb", line 507, in handle_request
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/puma-2.11.2/lib/puma/server.rb", line 375, in process_client
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/puma-2.11.2/lib/puma/server.rb", line 262, in block in run
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/puma-2.11.2/lib/puma/thread_pool.rb", line 104, in call
  File "/Users/dariusgoore/development/blackops/.bundle/gems/ruby/2.2.0/gems/puma-2.11.2/lib/puma/thread_pool.rb", line 104, in block in spawn_thread

This is a development issue. It can be closed.


RFC: avoid using Classical.em to split ifs

Description
The fact that Lean uses classical axioms on occasion to avoid fiddling with decidabilty instances is well-known and mostly harmless. However, there are some cases where this is not necessary, such as with the split tactic because the decidability instance is provided with the ite/dite expression and could be used to avoid using Classical.em.
Steps to Reproduce
theorem ifthisthenthat (n : Nat) : (if n = 0 then 0 else 0) = 0 := by split <;> rfl

#print axioms ifthisthenthat

Expected behavior: 'ifthisthenthat' depends on no axioms
Actual behavior: 'ifthisthenthat' depends on axioms: [Classical.choice, Quot.sound, propext]
Versions
Lean (version 4.0.0-nightly-2023-07-24, commit 3b6bc4a87df3, Release)
Additional Information
Tentative patch at PR #2412

People probably already know from my post on #2412, but I very much support fixing this issue. There is a fair amount of lean 3 / mathlib code which worked without classical axioms, and one of my published papers actually includes a theorem (from mathlib) which is claimed to be proved without choice, but this whole development took a major setback in the move to lean 4 because choice is used superfluously in a few critical dependencies.
Std plans to maintain the choice-freedom of most of the decidable parts of the theory, and I deployed some tools to help track regressions, but I quickly discovered that split was producing classical dependencies unnecessarily. I got as far as independently writing the fix from #2412 and confirming that it improved the situation significantly, but I did not attempt to submit the patch at the time. Now @fgdorais has written it independently, and I think he has done a good job of it.
I do not think that tracking classical axioms should be a major focus of lean 4. Most users do not need to care about this. However, it should be a (lightly) supported configuration, and I am willing to pitch in here and there to address issues, especially as they are likely to show up transitively in the std regression tests for this.

Here are some questions we expect every RFC should respond from now on.
User Experience: How does this feature improve the user experience?
Beneficiaries: Which Lean users and projects do benefit most from this feature/change?
Community Feedback: Have you sought feedback or insights from other Lean users?
Maintainability: Will this change streamline code maintenance or simplify its structure?
I will include them in the contribution guidelines.

one of my published papers actually includes a theorem (from mathlib) which is claimed to be proved without choice, but this whole development took a major setback in the move to lean 4.

I am assuming paper is using Lean 3, and the claim is still true.
Why depending on choice is so bad? What the new dependency is preventing you from doing? Could you explain the project? How impactful is it?

Dear Leo,
As the author of both the contentious PR and this RFC, I think I should say a few words about my perspective on this.
First and foremost, I sincerely apologize for not following guidelines for the PR. This was a mistake on my part but it was not done with harmful intent. I honestly thought at the time that I was submitting the PR in a black hole, so it didn't make sense to go through formalities. I just wanted to say: "Hey! It's not complicated to fix this!"
Second, I think your RFC questions are very good. I fully intend to get back to these soon.
 Let me preface this answer with a disclaimer: I am a logician. I do work in and enjoy foundations of mathematics including constructive logic from time to time. I do have deep knowledge of these areas. That said, I am not a constructivist and I do not think the axiom of choice is bad in any way for mathematical purposes. However, I do understand how classical reasoning can sometimes be harmful for reasoning about programs.
The main issue with split using Classical.em is that it's bad code. It opens a door that could theoretically be exploited by a malicious agent. Remember that Classical.em (Classical.choice, which is used to derive Classical.em, is even worse) can easily be used to prove that something non-computable is actually total. Since Lean relies on such tactics to prove termination there is always a chance for a bad leak to occur. To the best of my knowledge, it is not currently possible to use split to prove something that couldn't be proved without Classical.em, so this is harmless and I am not very concerned about this eventuality. But Lean keeps evolving and this is a potential sinkhole. The best way to avoid this is to avoid using Classical.em in Lean core and Std code so that bad code can only come from other parties.
Lean has a small kernel which is hard to dupe but it's a bad idea to only use that as a defense against malicious agents. I am not malicious enough to bring an example how to abuse split and other tactics but I hope you understand my concern.
Best wishes,
François G. Dorais

Dear François,
You have to be more concrete. You mention a hypothetical exploit, but then say you are not malicious enough to bring an example.

I do understand how classical reasoning can sometimes be harmful for reasoning about programs.

Where is the evidence/data to support this claim? Isabelle/HOL is based on classical reasoning and has a very successful track record on software verification (e.g., seL4 project.)
Note that even if you are correct, your PR does not fully solve the problem: If the decidability instance has loose bound variables you still fallback to classical. If we merge this PR, I can see users asking in the future: why do split sometimes use Classical.em, and we (the Lean developers) are the ones that have to address this question.
We are always listening to our users. We have talked to many mathematicians and computer scientists, and the vast majority don't care about constructivism. I have asked about high impact projects that are currently blocked unnecessary uses of Classical.em, and never got a convincing answer :)
Best,
Leo

Dear Leo,
I will not purposefully write code with the intent to break Lean. That's obviously pointless and I don't have that kind of time! (Even if I did, I wouldn't post it here, I would privately email you and ask what to do next.)
Note that I was specifically referring to termination proofs when I said it was bad code. I have no concerns with using classical logic elsewhere. Remember that even the halting problem is provably total using Classical.em!
It's been a while since I actively used Isabelle and HOL (mostly because Lean is so much better!) but I don't recall either one using classical logic for termination proofs. If I recall correctly, that question doesn't actually make sense for one of them and I suspect the other one is like that too but I don't want to make any claim without proof for either one, so please correct me if I'm wrong. In any case, I don't understand why you are referencing these. They're not designed as programming languages in the same way as Lean.

Note that even if you are correct, your PR does not fully solve the problem: If the decidability instance has loose bound variables you still fallback to classical. If we merge this PR, I can see users asking in the future: why do split sometimes use Classical.em, and we (the Lean developers) are the ones that have to address this question.

As you can see from the PR history, this was done after a comment from @digama0 so as to not break current behavior for split. If you think that's wrong, it's easy to fix and revert to the original behavior.
Best wishes,
François

Dear François,

I will not purposefully write code with the intent to break Lean. That's obviously pointless and I don't have that kind of time! (Even if I did, I wouldn't post it here, I would privately email you and ask what to do next.)

I never claimed you were writing code with the intent to break Lean. Sorry for the misunderstanding. I just pointed out that the Lean developers are the ones that review and maintain external contributions.

Note that I was specifically referring to termination proofs when I said it was bad code.

Same question still applies. Where is the evidence/data to support this claim?
Best,
Leo

Note that even if you are correct, your PR does not fully solve the problem: If the decidability instance has loose bound variables you still fallback to classical. If we merge this PR, I can see users asking in the future: why do split sometimes use Classical.em, and we (the Lean developers) are the ones that have to address this question.

I don't think either I or François have much interest in the case where the decidability instance has bound variables not in the condition itself, as this is very much an edge case which is unlikely to come up in practice. The two reasonable behaviors here are failing and using Classical.em. The latter has the advantage that for people who don't care about avoiding classical logic (which we anticipate to be most users), there is no loss in effectiveness in this case. The former has the advantage that the code is simpler and the algorithm and visible behavior is easier to explain, and also people who want to avoid classical logic in all cases can use split freely without worries. Do you have any particular preferences regarding weighing these two options?

Here are my answers to the updated RFC questions itemized by Leo earlier.

User Experience: How does this feature improve the user experience?

It will improve trust. Lean's small kernel is a key feature for trustworthiness. Axioms are necessary (e.g. to support quotient types, another key feature of Lean) but they bypass the kernel. Avoiding axioms when they are not necessary is a good way to ensure trust since axioms are blindly trusted by the kernel.

Beneficiaries: Which Lean users and projects do benefit most from this feature/change?

Although many users would not notice the change (which is good thing) increased trustworthiness would benefit everyone.

Community Feedback: Have you sought feedback or insights from other Lean users?

Yes. This was discussed here, on Zulip and private channels. The vast majority of community members that expressed opinions are favorable to this change. There are still corner issues but, to the best of my knowledge, these can be resolved at the PR phase.

Maintainability: Will this change streamline code maintenance or simplify its structure?

The tentative PR is relatively simple and designed to avoid disrupting any existing code to the extent possible. It is also designed to facilitate future code to avoid using unnecessary axioms while maintaining the possibility to fall back on classical axioms when necessary. I do not expect any issues beyond normal code maintenance. This can be further analyzed in the PR phase.

It will improve trust. Lean's small kernel is a key feature for trustworthiness. Axioms are necessary (e.g. to support quotient types, another key feature of Lean) but they bypass the kernel. Avoiding axioms when they are not necessary is a good way to ensure trust since axioms are blindly trusted by the kernel.

Classical.em is a well studied axiom. There are no trust concerns.

Although many users would not notice the change (which is good thing) increased trustworthiness would benefit everyone.

There are no trust concerns. Moreover, Mathlib uses classical reasoning in many different places anyway.

The vast majority of community members that expressed opinions are favorable to this change.

You need to provide evidence. To be precise, "don't care about this feature"  is not support.

You need to provide evidence. To be precise, "don't care about this feature" is not support.

Hi Leo! I would like to express support for adding this feature. I entirely agree that there are no trust concerns regarding Classical.em. My motivation is different, and it is that weaker theories have more models (Neel's remark here). Specifically, a Lean proof that does not depend on Classical.em can be taken to mean other things than just its set-interpretation by virtue of being interpretable in models other than Mario's set-based model. This has practical applications: if a specific model of a subset of Lean's theory is formalized in Lean, such Lean theorems can be viewed as proving something about that model and be made to actually prove that using custom elaborators.

@Vtec234 Thanks for sharing your view.

My motivation is different, and it is that weaker theories have more models (Neel's remark here).

While I understand that weaker theories can have more models, my experience has shown that their practical applications have been limited to mostly hypothetical ones. Are there any specific, impactful projects that will benefit directly from this feature? So far, I've come across only hypothetical proposals.
My primary concern is receiving numerous PRs that attempt to avoid classical reasoning in various parts of the system without a compelling rationale. This can easily lead us down a path where contributors may soon try to sidestep constructs like funext in tactics like simp.
You might recall that we experimented with supporting multiple flavors of type theory in the past. Unfortunately, it turned out to be a substantial time sink. Given how valuable time is, it's crucial that we prioritize. We're in a unique position now, with the project receiving ample funding. It's imperative that we allocate these resources judiciously.
Moreover, we are planning to add more automation to Lean in the near future, and we will not waste any resources trying to avoid classical principles.

Are there any specific, impactful projects that will benefit directly from this feature?

I am working on one. But it is very much in progress, and I would entirely understand if the dev team does not want to add features to support a potential future package.

Dear Leo,

I do understand how classical reasoning can sometimes be harmful for reasoning about programs.

Where is the evidence/data to support this claim?

This is well-known and I mentioned the canonical example: the solution to the halting problem is provably total using Classical.em but it is provably not computable.

Isabelle/HOL is based on classical reasoning and has a very successful track record on software verification (e.g., seL4 project.)

I was delighted to read about seL4, thank you for mentioning that, it's a really fascinating project!
That said, after reading a bit more, I'm now nearly 100% sure Isabelle always uses LCF (no matter what flavor) for soundness. So I don't understand what you're trying to say here about classical reasoning.
Best wishes,
François

My primary concern is receiving numerous PRs that attempt to avoid classical reasoning in various parts of the system without a compelling rationale. This can easily lead us down a path where contributors may soon try to sidestep constructs like funext in tactics like simp.

If the proof requires funext, then there isn't any issue with doing so. I don't think there is any slippery slope here, there are one or two issues in core tactics which will unlock a huge amount of downstream work. That's all this is. I know you don't consider this work important, but other people do, and I don't see why in an individual RFC like this we need to be considering future RFCs. If a future RFC wants to consider removing funext in simp, let that be considered separately on its own merits.

Dear Leo,

You have to be more concrete. You mention a hypothetical exploit, but then say you are not malicious enough to bring an example.

Let me try! There's three scenarios, the "hypothetical exploit" is the third. Retrospectively, I'm realizing the second scenario is the only one I really care about.
Scenario 1. Since Classical.choice, Classical.propDecidable and friends are not computable, it doesn't make sense for a def with executable code to honestly depend on these. If it really did, it wouldn't compile. Yet that happens all the time. This example is due to Jun Yoshida, and it happens even after split is fixed as suggested by this RFC.
def test : List Nat → Nat
| [] => 0
| 0 :: l => test l
| (n+1) :: l => 1 + test (n :: l)

-- 'test' depends on axioms: [Classical.choice, Quot.sound, propext]
#print axioms test

The reason is that this definition uses well-founded recursion, the termination proof depends on theorems from Init.Data.Nat.Linear that use the by_cases tactic. That tactic systematically uses Classical.em but it is not currently part of this RFC to fix this tactic.
I consider this behavior to be harmless. The kernel saw through the spurious dependency, the code got generated and it works exactly as expected.
(Also note that Classical.em is not itself problematic since it lives in Prop. If it showed up as an axiom instead of Classical.choice, I would immediately know it's not relevant.)
Scenario 2. This is a flipped view of part 1. Suppose I write a def but I make a typo, I wanted to use X but I typed Y. They both have the same type, so everything type checks, but Y is noncomputable. At some point, I get the error:
failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.choice', and it does not have executable code

I know my code should compile, so I know I made an error somewhere. I start digging using #print axioms to see where that dependency on Classical.choice comes from. To my dismay, there are many parts that depend on Classical.choice. I will probably eventually find Y but since by_cases, split and simp are common tactics, there's a lot of noise.
At worst, this behavior can be characterized as unhelpful. I think this is sufficient motivation to fix, but I would also consider other options. For example, as a better #print axioms for defs that filters out the noise. That route is arguably better since fixing by_cases, split and simp would definitely cut down the noise, it wouldn't actually resolve the issue of irrelevant dependencies as a whole. That said, I have no idea how to implement such a noise filtering #print axioms.
Scenario 3. Suppose there's a bug in the kernel whereby some noncomputable definition somehow ends up generating bogus code. This is extremely unlikely. I can't imagine how that could happen and I hope we never find out.
Let's say code using such a def lands on my review queue. (Either produced by a malicious agent or as a result of a coding error.) The code compiles fine, it comes with a test suite that (cleverly or mistakingly) avoids the bug. Reading through the code and the tests doesn't reveal any issues, #print axioms shows some weird noncomputable dependencies but I know that happens all the time so I ignore that suspicious data. I rubber stamp the code and move on to the next review item.
This would be terrible! But it is also extremely unlikely. Lean maintainers can't possibly spend much time fixing hypothetical disasters like this. It's much more important to spend time writing quality code which is less likely to have bugs in the first place. I'm sorry I brought that up earlier, I have a bad habit for catastrophizing that I evidently need to keep working on.
Best wishes,
François

Scenario 1. Since Classical.choice, Classical.propDecidable and friends are not computable, it doesn't make sense for a def with executable code to honestly depend on these. If it really did, it wouldn't compile. Yet that happens all the time.

A def can be computable while still depending on classical axioms. The reason is because the axiom can be used inside computationally irrelevant parts of the definition, e.g. proof arguments or type arguments. In particular, any theorem which is proved using choice is computationally irrelevant (that is, "vacuously computable"), and in fact Classical.em is just such a theorem (proved using Classical.choice despite this being noncomputable).
def foo (n : Nat) (_h : n > 0) : Nat := n + 1

def bar : Nat := foo 1 <| by
  by_cases 2 + 2 = 4 <;> exact Nat.succ_pos _

#eval bar -- 2
#print axioms bar
-- 'bar' depends on axioms: [Classical.choice, Quot.sound, propext]

Scenario 2. This is a flipped view of part 1. Suppose I write a def but I make a typo, I wanted to use X but I typed Y. They both have the same type, so everything type checks, but Y is noncomputable. At some point, I get the error:
failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.choice', and it does not have executable code

I know my code should compile, so I know I made an error somewhere. I start digging using #print axioms to see where that dependency on Classical.choice comes from.

For the same reason as the above, this is the wrong way to diagnose noncomputability issues, because things can be noncomputable without using Classical.choice and vice versa. You should instead look directly at the error message, which points to a noncomputable direct dependency used in the definition in a computationally relevant way. It is difficult to typo this unless you use noncomputable section because each definition individually marks whether it is noncomputable.

Scenario 3. Suppose there's a bug in the kernel whereby some noncomputable definition somehow ends up generating bogus code. This is extremely unlikely. I can't imagine how that could happen and I hope we never find out.

I don't really understand this hypothetical. At least right now, noncomputable definitions are exactly those for which the compiler cannot generate a definition for one reason or another. If the compiler is able to generate code, bogus or otherwise, then it will not need to be marked noncomputable, and if you do mark a definition as noncomputable then the compiler doesn't generate code for it at all, bogus or otherwise.

Scenario 1. Since Classical.choice, Classical.propDecidable and friends are not computable, it doesn't make sense for a def with executable code to honestly depend on these. If it really did, it wouldn't compile. Yet that happens all the time.

A def can be computable while still depending on classical axioms. The reason is because the axiom can be used inside computationally irrelevant parts of the definition, e.g. proof arguments or type arguments. In particular, any theorem which is proved using choice is computationally irrelevant (that is, "vacuously computable"), and in fact Classical.em is just such a theorem (proved using Classical.choice despite this being noncomputable).

That's pretty much exactly what I'm saying, isn't it? I even made that same remark about Classical.em vs Classical.choice.

Scenario 2. This is a flipped view of part 1. Suppose I write a def but I make a typo, I wanted to use X but I typed Y. They both have the same type, so everything type checks, but Y is noncomputable. At some point, I get the error:
failed to compile definition, consider marking it as 'noncomputable' because it depends on 'Classical.choice', and it does not have executable code

I know my code should compile, so I know I made an error somewhere. I start digging using #print axioms to see where that dependency on Classical.choice comes from.

For the same reason as the above, this is the wrong way to diagnose noncomputability issues, because things can be noncomputable without using Classical.choice and vice versa. You should instead look directly at the error message, which points to a noncomputable direct dependency used in the definition in a computationally relevant way.

It's obviously the wrong way to do this since it doesn't work! The error message for noncomputability is not that specific. The one above was copy pasted from an actual constructed example, there is no location information at all. To be honest, I edited Classical.propDecidable to Classical.choice since there was no reason to bring up Classical.propDecidable. Oh! Is that what you're pointing out? The name info is narrower? I didn't pay attention since I generated the error on purpose.

There is one exception to this, which is that by_cases uses classical logic even if the goal is not a proposition, resulting in a proof approach that fails:

The Std patch to by_cases is good. That's why I didn't consider it important to fix by_cases in this RFC.

Scenario 3. Suppose there's a bug in the kernel whereby some noncomputable definition somehow ends up generating bogus code. This is extremely unlikely. I can't imagine how that could happen and I hope we never find out.

I don't really understand this hypothetical. At least right now, noncomputable definitions are exactly those for which the compiler cannot generate a definition for one reason or another. If the compiler is able to generate code, bogus or otherwise, then it will not need to be marked noncomputable, and if you do mark a definition as noncomputable then the compiler doesn't generate code for it at all, bogus or otherwise.

It's a silly scenario. The disaster is that bogus code ends up being generated in a manner that could be avoided if the #print axioms info was more useful. I like being able to detect bogus code before it goes into production.

It's a silly scenario. The disaster is that bogus code ends up being generated in a manner that could be avoided if the #print axioms info was more useful. I like being able to detect bogus code before it goes into production.

I'm not seeing how it does that. #print axioms is doing exactly what it is designed to do, and it has very little to do with the code generation process.

If you're honestly suspend disbelief and engage in my Scenario 3 fiction, then I'm willing to flesh out some details from my imagination.
 There's two key things to defeat, type checking and code generation. The agent comes up with a strategy to add an axiom with a type signature that would dupe pass the type check. The axiom may be further disguised in syntax to escape visual check. The agent gains control of the Lean source code and creates a hole that inserts the bad code instead of failing when it encounters that particular axiom name. I don't know why nobody noticed but since that axiom name doesn't occur anywhere in Lean, it's unlikely to make any tests fail. (Continue with the rest of Scenario 3 but, since it's my imagination, replace the part where #print axioms doesn't work with the following.) Fortunately, Lean recently fixed its issues with #print axioms and I have a habit of using it as part of my review process since I personally dislike unnecessary axioms, I locate the strange axiom and catch the malicious agent in the act!
Does this actually make sense? Probably not and hopefully not. Could the malicious agent do the same without using axioms? Sure, why not. Should Lean be in any way worried about this kind of scenario? Absolutely not. Should some TLA government organization that uses Lean be worried about unnecessary axioms this way? I don't know. Let's make a movie about it!

Regarding Scenario 2. I think your right, #print axioms is not the right tool here. That scenario is looking less and less compelling to me since this RFC wouldn't actually fix anything there.
With all three scenarios being non-compelling, I think I'm slowly converging to Leo's view. Not quite though, I still think my PR code is better than the current code since it allows more options without adding much complexity. I don't know how to argue that as a motivation for this RFC.

I know I travel in heavily constructivist circles, but when trying to sell Lean to CMU PL people, non-constructivism is brought up relatively frequently. Of course, PL people are not the target audience, and constructivism is not the target logic, but it would be nice to at least accommodate constructivism when it's easy to do so.

My primary concern is receiving numerous PRs that attempt to avoid classical reasoning in various parts of the system without a compelling rationale.

I totally understand this. In particular, having more complex tactic implementations in core means they could be harder to maintain in the future. I'm not very familiar with the code base, but the maintenance burden for this particular RFC seems pretty low, at least based on the implementation in #2412. Maybe that's something to worry about down the road?

This issue has been incidentally fixed by #4349: The MWE in the first message is now axiom-free. :tada:


Should we mention Inferno/Nervjs?

While Preact and Inferno have a slightly more complicated migration from React (because of incompatibilities, you have to install additional libraries for the transition groups etc), Nervjs does not.
Also, Inferno is much faster than Preact, while being also larger. But migration is even harder in my experience.
NervJS migration is painless and it seems to be overall faster than React and Preact and in some cases faster than Inferno.
See here for more details: https://github.com/NervJS/nerv/issues/10

Want to make a PR? :–)

Yup, I'll do it soon :)

Sorry for taking so long!

No problem :–)


Switch from PhantomJs to Headless Chrome

I tried to index site, but some steps failed. I restarted with same command and got same error.
BTW @charlesmike posted link to logs, but I didn't find them on page: http://charles.amihaiemil.com/logs.html?log=/887c5b90-1aa5-46e8-9357-3f692e37badc.log

Index site sometimes fails bc phantomjs and selenium are quite volatile... trouble when navigating. I'll migrate it to headless chrome as soon as I have some time. In the meantime, try index sitemap, I never had issues with that one.
The logs should display fine, never had issue with them either. Can you maybe open an issue about that, with the link that doesnt work?

@g4s8 apparently, AWS Free Tier is so cheap, that the server's memory is occupied with log files...:
  java.io.IOException: No space left on device

cleaning up now...

@g4s8 cleaned and restarted, it should work fine now. Even index site should work for your blog, since it has a few pages only. If not, index sitemap or index page :)

@amihaiemil thanks, now I can read logs. Index sitemap command also working fine.
Here new link to logs with index site failing: http://charles.amihaiemil.com/logs.html?log=/f6754fb4-baec-467a-b10b-d0fc674c8d62.log

Yes, it's definetely phantom + selenium, I had the same errors


Microsoft.Azure.Management.ApiManagement on NuGet has totally different class members.

Using https://www.nuget.org/packages/Microsoft.Azure.Management.ApiManagement/3.4.0-preview (which has a publish date earlier than the inititial check in of https://github.com/Azure/azure-sdk-for-net/tree/psSdkJson6/src/SDKs/ApiManagement) and looking in to Microsoft.Azure.Management.ApiManagement.IUserOperations I see methods like CreateAsync and DeleteAsync.
If I look at https://github.com/Azure/azure-sdk-for-net/blob/3bd40fa47229b3a9163ffefc05cbc5f591c85f51/src/SDKs/ApiManagement/Management.ApiManagement/Generated/IUserOperations.cs I see methods like CreateOrUpdateWithHttpMessagesAsync or DeleteWithHttpMessagesAsync.
Is the 3.4.0-preview NuGet package very out of date or am I using the wrong package to get the .NET wrapper for these Api Management api's?

@leftler The package version published from the psSdkJson6 codebase (here) is 4.0.0-preview which, as expected has the CreateOrUpdateWithHttpMessagesAsync or DeleteWithHttpMessagesAsync methods in Microsoft.Azure.Management.ApiManagement.IUserOperations interface.
The 3.4.0-preview version was published from the codebase here
You could upgrade to 4.0.0-preview version to see this code.

If you have any further issues while using the package, kindly reopen the issue and provide detailed repro steps.


[UI] Shift the Create pattern btn

Current Behavior
Currently, the pattern create button is at the bottom of the datable/
Desired Behavior
Relocate this button to the top in the line of other import options
Implementation

We are using MUIDatable here, and a custom toolbar with custom options to add new import or any other feature to the table.
Referring to the previous custom components under the custom toolbar will help.

Acceptance Tests

Import should work as earlier.
give a "+" to create a new pattern (just convert/replace the old create btn with an icon)

Mockups
Shift this to top(in table toolbar)

Here

Contributor Guides and Resources

🎨 Wireframes and designs for Meshery UI in Figma
🖥 Contributing to Meshery UI
🙋🏾🙋🏼 Questions: Layer5 Discussion Forum and Layer5 Community Slack

I like to work on this.

Sure @asubedy.


fix(art-quiz): update results page copy

The type of this PR is: fix

This PR solves GRO-1531
Description
Swap out copy in translations.json

Appears to have a related spec failure


BUG: Plus icon interferance with accordian text

Is there an existing issue for this?

[X] I have searched the existing issues

What happened?
With every accordian item, in beginning of text there slight interfarce of text with some transparent icon.
Record

[X] I agree to follow this project's Code of Conduct
[X] I'm a GSSOC'24 contributor
[X] I want to work on this issue

@Kalivarapubindusree please assign me this issue under GSSOC'24 label.

Please fix there are two FAQs fix them in one section @saadakbar1


[v1.3] Add checkout upcoming booking feature

checkout will double as a booking_delete command.

https://github.com/CS2103-AY1819S1-F11-2/main/issues/56 Refer to this issue for previous brainstorming pointers.


fixes to hsic.py

Ok, this is the correct branch to create pull request  -- same coment as the one i closed. this one has only one file.
Hi Kurt, I used 3 functions from hsic and noticed a few things
you can allocate much less memory by using in place functions, one shouldnt do that in the model but in the loss function that is ok, because loss is the source of of the gradient it simply copies the value to the grad.
for some reason your kernelmat you cast a new tensor in the -e^(d/v), i removed that - so now if X device is cuda, the device doesnt die. Also, recasting a Float Tensor introduces floating point errors, not significant in this context but i dont know how they would propagate.
I added a linting mute so my vscode doesnt flag torch. or as wrong

If you want look at the reasoning, tests and timing, I have a jupyter in my dev branch where I tested the changes.
https://github.com/xvdp/HSIC-bottleneck/blob/xvdp_dev/jupyter/HSIC_Kernel.ipynb
I only changed the 3 functions that i was using
distmat()
kernelmat()
hsic_normalized_cca()

oh T-H-A-N-K-S!
I'll spend days after work to test your code. I'll confirm with you shortly.

no worry. I only touched 3 functions - that I needed. if you really want to
speed it up you could write it in cuda and save yourself allocation of all
those eye matrices, and since much of the code results in symmetric
matrices, probably need half or even less computation.
alternatively, I just saw a sparse cuda matrix library -
https://github.com/huggingface/pytorch_block_sparse
last but not least as a general speed optimization with pytorch, therse a
nice tutorial from nvidia,   https://www.youtube.com/watch?v=9mS1fIYj1So
but thats a general reference. Im more interested in the idea that hsic()
or another type of information measure could replace end to end backprop. -
OR be used in combination with... thanks for the work.
On Tue, Sep 8, 2020 at 7:14 PM Leopad<EMAIL_ADDRESS>wrote:

oh T-H-A-N-K-S!
I'll spend days after work to test your code. I'll confirm with you
shortly.
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
https://github.com/choasma/HSIC-bottleneck/pull/6#issuecomment-689255259,
or unsubscribe
https://github.com/notifications/unsubscribe-auth/AJYHPOWML7CG5XYD5UKSILLSE3QJXANCNFSM4Q42PU2A
.


🚨 This example is very old and will soon be replaced

I am working on this: https://github.com/aws/containers-roadmap/issues/1876
Which will provide a much better experience. Some work in progress is here: https://github.com/aws/aws-for-fluent-bit/pull/499
Once the new daemon is released, this repo should be archived or a note should be added that its no longer recommended.

@PettitWesley is it still a WIP?

@Alonreznik its been put on hold for now, hopefully I will get back to it some time.


Mechanism for generating proposal ID

This proposal documents the mechanism for generating proposal ID implemented in
go-perun PR#167 and the rationale behind it.

@matthiasgeihs I have summarized all the points from our discussion into a draft proposal. Could you have a look into it ?
I have left point 3 in the possible scenarios where proposal ID could be same for two proposals as a TODO.