Aaron Hill Aaron1011
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| curl https://api.x.ai/v1/chat/completions -H "Content-Type: application/json" -H "Authorization: Bearer $XAI_API_KEY" -d '{"messages":[{"role":"user","content":"What is the name of the capital city of Japan?"}],"model":"grok-3-mini","response_format":{"type":"json_object"},"stream":false}' |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| -- TODO - upstream to mathlib | |
| lemma x_log_x_tendsto_atTop: Filter.Tendsto ((fun x => x⁻¹) ∘ fun x => Real.log x / x) Filter.atTop Filter.atTop := by | |
| apply Filter.Tendsto.comp (f := fun x => Real.log x / x) (g := fun x => x⁻¹) (x := Filter.atTop) (y := (nhdsWithin 0 (Set.Ioi 0))) (z := Filter.atTop) | |
| . | |
| exact tendsto_inv_nhdsGT_zero (𝕜 := ℝ) | |
| . | |
| rw [tendsto_nhdsWithin_iff] | |
| refine ⟨?_, ?_⟩ | |
| . | |
| have log_div_x := Real.tendsto_pow_log_div_mul_add_atTop 1 0 1 (by simp) |
Aaron1011
/ bad_refcell_error.rs
Created
April 18, 2025 18:26
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| use std::cell::RefCell; | |
| struct Wrapped { | |
| first: bool, | |
| second: bool | |
| } | |
| fn main() { | |
| let a = RefCell::new(Wrapped { | |
| first: true, |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Mathlib | |
| lemma foo: Filter.Tendsto ((fun x => x⁻¹) ∘ fun x => Real.log x / x) Filter.atTop Filter.atTop := by | |
| have bar := Filter.Tendsto.comp (f := fun x => Real.log x / x) (g := fun x => x⁻¹) (x := Filter.atTop) (y := (nhdsWithin 0 (Set.Ioi 0))) (z := Filter.atTop) ?_ ?_ | |
| . | |
| exact bar | |
| . | |
| exact tendsto_inv_nhdsGT_zero (𝕜 := ℝ) | |
| . | |
| rw [tendsto_nhdsWithin_iff] |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| fof(eq1, hypothesis, ! [X] : X = X). | |
| fof(eq2, hypothesis, ! [X] : ! [Y] : X = Y). | |
| fof(eq3, hypothesis, ! [X] : X = mul(X, X)). | |
| fof(eq4, hypothesis, ! [X] : ! [Y] : X = mul(X, Y)). | |
| fof(eq5, hypothesis, ! [X] : ! [Y] : X = mul(Y, X)). | |
| fof(eq6, hypothesis, ! [X] : ! [Y] : X = mul(Y, Y)). | |
| fof(eq7, hypothesis, ! [X] : ! [Y] : ! [Z] : X = mul(Y, Z)). | |
| fof(eq8, hypothesis, ! [X] : X = mul(X, mul(X, X))). | |
| fof(eq9, hypothesis, ! [X] : ! [Y] : X = mul(X, mul(X, Y))). | |
| fof(eq10, hypothesis, ! [X] : ! [Y] : X = mul(X, mul(Y, X))). |
Aaron1011
/ gist:9cf66232619fd336e993dbaa76b82e48
Created
December 4, 2023 01:28
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (lldb) process attach --pid 6936 | |
| Process 6936 stopped | |
| * thread #9, stop reason = [31mException 0x80000003 encountered at address 0x7ff8f9f03d80[0m | |
| frame #0: [33m0x00007ff8f9f03d81[0m ntdll.dll`DbgBreakPoint + 1 | |
| ntdll.dll`DbgBreakPoint: | |
| [33m-> [0m 0x7ff8f9f03d81 <+1>: retq | |
| [33m [0m 0x7ff8f9f03d82 <+2>: int3 | |
| [33m [0m 0x7ff8f9f03d83 <+3>: int3 | |
| [33m [0m 0x7ff8f9f03d84 <+4>: int3 | |
| Executable module set to "D:\a\ruffle\ruffle\target\debug\deps\tests-8b6a3f6194ee2f95.exe". |
Aaron1011
/ gist:479c460250ed9ead4e0e6631a2535071
Created
June 22, 2020 17:31
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 2020-06-22T07:22:58.9930522Z error: auxiliary build of "tests/ui/auxiliary/proc_macro_attr.rs" failed to compile: | |
| 2020-06-22T07:22:58.9930946Z status: exit code: 1 | |
| 2020-06-22T07:22:58.9942809Z command: "/checkout/obj/build/x86_64-unknown-linux-gnu/stage2-tools-bin/clippy-driver" "tests/ui/auxiliary/proc_macro_attr.rs" "-L" "/checkout/obj/build/x86_64-unknown-linux-gnu/stage2-tools/x86_64-unknown-linux-gnu/release/build/clippy-0fb70441c4c18d97/out/test_build_base" "--target=x86_64-unknown-linux-gnu" "--error-format" "json" "--out-dir" "/checkout/obj/build/x86_64-unknown-linux-gnu/stage2-tools/x86_64-unknown-linux-gnu/release/build/clippy-0fb70441c4c18d97/out/test_build_base/empty_line_after_outer_attribute.stage-id.aux" "-L" "/checkout/obj/build/x86_64-unknown-linux-gnu/stage2-tools/release/deps" "-L" "/checkout/obj/build/x86_64-unknown-linux-gnu/stage2-tools/x86_64-unknown-linux-gnu/release/deps" "-Dwarnings" "-Zui-testing" "--extern" "clippy_lints=/checkout/obj/build/x86_64-unknown-linux-gnu/stage2-tools/x8 |
Aaron1011
/ gist:94e97e3b5a7ba62f024ce4fda8211bdc
Created
April 6, 2020 01:08
Collectionstest tombstone
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** *** | |
| Build fingerprint: 'generic/sdk/generic:4.3.1/JB_MR2/3876170:eng/test-keys' | |
| Revision: '0' | |
| pid: 278, tid: 877, name: vec::test_try_r >>> /data/tmp/work/test1/collectionstests-8c9066a5b2aa9a17 <<< | |
| signal 11 (SIGSEGV), code 1 (SEGV_MAPERR), fault addr deadbaad | |
| Abort message: '@@@ ABORTING: invalid address or address of corrupt block 0xb7301030 passed to dlfree' | |
| r0 00000027 r1 b6bd9284 r2 00000000 r3 deadbaad | |
| r4 00000000 r5 b556529c r6 34b84000 r7 b7301038 | |
| r8 b72d5c28 r9 b7270b38 sl b72d5c28 fp b5565780 | |
| ip b7301038 sp b5565298 lr b6bac4fb pc b6bac524 cpsr 60000030 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #![feature(never_type)] | |
| //#![feature(never_type_fallback)] | |
| fn get_type<T>(_: T) -> &'static str { | |
| std::any::type_name::<T>() | |
| } | |
| fn unconstrained_return<T>() -> Result<T, String> { | |
| Err("Hi".to_string()) | |
| } |
Aaron1011
/ intrinsic_transmute
Created
October 3, 2019 00:49
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| [DEBUG rustc::ty::print] default_print_def_path: key=DefKey { parent: Some(DefIndex(924)), disambiguated_data: DisambiguatedDefPathData { data: ValueNs("transmute"), disambiguator: 0 } } | |
| [DEBUG rustc::ty::print::pretty] try_print_visible_def_path: def_id=DefId(2:965 ~ core[5cf2]::intrinsics[0]::[1]::transmute[0]) | |
| [DEBUG rustc::ty::print::pretty] try_print_visible_def_path: cur_def_key=DefKey { parent: Some(DefIndex(924)), disambiguated_data: DisambiguatedDefPathData { data: ValueNs("transmute"), disambiguator: 0 } } | |
| [DEBUG rustc::ty::print::pretty] try_print_visible_def_path: def_id=DefId(2:1114 ~ core[5cf2]::mem[0]) | |
| [DEBUG rustc::ty::print::pretty] try_print_visible_def_path: cur_def_key=DefKey { parent: Some(DefIndex(0)), disambiguated_data: DisambiguatedDefPathData { data: TypeNs("mem"), disambiguator: 0 } } | |
| [DEBUG rustc::ty::print::pretty] try_print_visible_def_path: def_id=DefId(1:0 ~ std[5758]) | |
| [DEBUG rustc::ty::print::pretty] try_print_visible_def_path: def_id=DefId(0:11 ~ bad_intrinsic[317d]::std[0]) |
NewerOlder