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
pdfcrop %~nx1 |
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
status key command | |
Composition Backspace Backspace | |
Composition Ctrl a MoveCursorToBeginning | |
Composition Ctrl Backspace Backspace | |
Composition Ctrl d MoveCursorRight | |
Composition Ctrl Down MoveCursorToEnd | |
Composition Ctrl e MoveCursorToBeginning | |
Composition Ctrl Enter Commit | |
Composition Ctrl f MoveCursorToEnd | |
Composition Ctrl g Delete |
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
#include <iostream> | |
#include <map> | |
#include <set> | |
#include <string> | |
#include <vector> | |
using namespace std; | |
#define repi(itr, ds) for (auto itr = ds.begin(); itr != ds.end(); itr++) |
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 torch | |
import timm | |
import torch.neuron | |
# original model | |
model = timm.create_model("fbnetc_100", pretrained=True) | |
model.eval() | |
# number of parameters |
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
INFO:Neuron:There are 1 ops of 1 different types in the TorchScript that are not compiled by neuron-cc: aten::adaptive_max_pool2d, (For more information see https://github.com/aws/aws-neuron-sdk/blob/master/release-notes/neuron-cc-ops/neuron-cc-ops-pytorch.md) | |
INFO:Neuron:Number of arithmetic operators (pre-compilation) before = 306, fused = 295, percent fused = 96.41% | |
INFO:Neuron:Compiling function _NeuronGraph$868 with neuron-cc | |
INFO:Neuron:Compiling with command line: '/home/ubuntu/anaconda3/envs/aws_neuron_pytorch_p36/bin/neuron-cc compile /tmp/tmp1qen5wtt/graph_def.pb --framework TENSORFLOW --pipeline compile SaveTemps --output /tmp/tmp1qen5wtt/graph_def.neff --io-config {"inputs": {"0:0": [[1, 5, 3, 384, 384], "float32"]}, "outputs": ["Reshape_2:0"]} --verbose 35' | |
.[01:48:52] /opt/brazil-pkg-cache/packages/DmlcTvm/DmlcTvm-1.7.2.0/AL2_x86_64/generic-flavor/src/src/relay/pass/do_replication.cc:66: Replication is not applied to group convolution. Kernel and data input channels do not match[3, 3, 4, 128] [ |
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
#!/bin/bash | |
tmpdir=$(mktemp -d) | |
gs -sDEVICE=pdfwrite -dCompatibilityLevel=1.4 -o $tmpdir/tmp.pdf $1 | |
pdfcrop $tmpdir/tmp.pdf $1 |
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
Ltac split_all := try _split_all | |
with _split_all := | |
match goal with | |
| |- (_ /\ _) => try (repeat split) || split_all | |
end. | |
(* 以下は動作確認用 *) | |
Lemma bar : | |
forall P Q R S : Prop, |
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
Require Import Arith. | |
Require Import Omega. | |
Require Import Recdef. | |
Function log(n:nat) {wf lt n} := | |
if le_lt_dec n 1 then | |
0 | |
else | |
S (log (Div2.div2 n)). | |
Proof. |
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
Ltac split_all := try (repeat split)||split_all. | |
(* 以下は動作確認用 *) | |
Lemma bar : | |
forall P Q R S : Prop, | |
R -> Q -> P -> S -> (P /\ R) /\ (S /\ Q). | |
Proof. | |
intros P Q R S H0 H1 H2 H3. | |
split_all. |
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
(* bindの記法を予約 *) | |
Reserved Notation "x >>= y" (at level 110, left associativity). | |
(* モナド *) | |
Class Monad(M:Type -> Type) := { | |
bind {A B} : M A -> (A -> M B) -> M B | |
where "x >>= f" := (bind x f); | |
ret {A} : A -> M A; | |
left_id : forall {A:Type} {B:Type} (x:A) (f:A -> M B), ((ret x) >>= f) = (f x); | |
right_id : forall {A:Type} (x:M A), (x >>= ret) = x; |
NewerOlder